Update of information in [AL0101T1] .
A new update of Isabelle, Isabelle94-2, is now on the Cambridge and Munich ftp sites, available .
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