Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Date: Fri, 9 Sep 1994 00:22:56 +1000
From: Malcolm Newey <Malcolm.Newey@cs.anu.edu.au>
Message-Id: <199409081422.AAA09971@achernar.anu.edu.au>
To: info-hol@leopard.cs.byu.edu


As some of you know, I have been working for several months on Edition 2
of the sets libraries that were last updated by Tom in early 1992.

The new features that I have been implementing are:
   i)    inspired by Ching-Tsun's ACI contrib library, I provide functions
         to lift associative and commutative binary operations (with
         or without identity) to operate over index sets.
   ii)   I privide the where-with-all to include set comprehensions
         such as {x+y in f(S) | y-z > 0}.
   iii)  I have some tactics that implement a decision procedure for a
         class of boolean set expressions.

The current libraries have conversions for about half of the standard
set operations when supplied with finite sets.  I have done the other half.

Although work ceased in July, a lot of progress was made towards updating
the HOL88 libraries.  The problem is that other activities will prevent
progress until the start of November.  (I am travelling.)

At that time, work that is virtually completed on the HOL88 finite sets
Library will be ported to all three libraries in both HOL88 and HOL90.

The point of this message is to alert Sets library users of the upcoming
enhancements so that you can talk to me about your views on what should be
in the sets libraries in 1995 and 1999.

See you in Malta.

Malcolm