Return-Path: Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <14615-0@swan.cl.cam.ac.uk>; Sat, 15 Feb 1992 01:27:12 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA10969; Fri, 14 Feb 92 17:07:03 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA10965; Fri, 14 Feb 92 17:06:47 -0800 Received: from scaup.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <14507-0@swan.cl.cam.ac.uk>; Sat, 15 Feb 1992 01:08:51 +0000 To: info-hol@edu.uidaho.cs.ted Cc: Tom.Melham@uk.ac.cam.cl Subject: sets (again). Date: Sat, 15 Feb 92 01:08:48 +0000 From: Tom.Melham@uk.ac.cam.cl Message-Id: <"swan.cl.ca.509:15.01.92.01.08.54"@cl.cam.ac.uk> This note is directed to users of the finite_sets library. I am just about begin work on a complete revision of this library for HOL88 version 2.01. The idea will be to make it as consistent as possible with the sets (and pred_sets) libraries. There are also a number of awkwardnesses with the finite_sets library that I hope to eliminate. I intend also to write a Manual. Users of finite_sets are invited to send me any comments they may have that might be relevant to this revision. Tom