[T4] ================================================ AMAST Links 02 02

		         Isabelle94-2 : Update 

   *Update* of information in [AL0101T1].
 
  A new update of Isabelle, Isabelle94-2, is now on the Cambridge and 
Munich ftp sites, available at
URL: ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-2.tar.gz

  Here is a summary of changes from Isabelle94-1.  Resolution is 
significantly faster.  The different sections in a .thy file can now 
be mixed and repeated freely.

  There is now a database of theorems for FOL, HOL and ZF. New commands
including qed, qed_goal and bind_thm store theorems in the database. At
present the database only allows simple queries: return a named theorem
(get_thm) or all theorems of a given theory (thms_of), or find out what
theory a theorem was proved in (theory_of_thm).  The database could be
useful to designers of user interfaces.

  Bugs have been fixed in the inductive definition and datatype
packages.  The classical reasoner provides deepen_tac and depth_tac,
making FOL_dup_cs and HOL_dup_cs obsolete. Syntactic ambiguities caused
by the new treatment of syntax in Isabelle94-1 have been removed.

  ZF has a new definition of function space; it is equivalent but 
easier to use. ZF also has many new results about cardinal and ordinal
arithmetic (some due to Krzysztof Grabczewski).  

  HOL now supports a 'subtype' facility for introducing new types as 
subsets of existing types.

  We expect to release updates like this every couple of months, 
instead of waiting a year between releases as before.  Many users will
not need to pick up each update.

  Larry Paulson and Tobias Nipkow