[T6] ================================================ AMAST Links 02 07

                    Isabelle Update: Isabelle94-4

   *Update of information in [AL0205T1].

  A new update of Isabelle, _Isabelle94-4_, is now on the Cambridge ftp
site at URL:
   ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-4.tar.gz
It is also on the _Munich site_, at URL:
   ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/
   Isabelle94-4.tar.gz

  Here's a summary of changes from Isabelle94-3.
  Space requirements are much reduced, thanks to changes to the parser
and classical reasoner.
  Theory files (.thy) no longer require \...\ escapes to break lines.
  You can search the theorem database.  See the section "Retrieving
theorems" on page 8 of the (updated) Reference Manual.
  There are new examples, especially Grabczewski's monumental case
study involving the Axiom of Choice.
  The previous version of HOL is now called Old_HOL. It will disappear
altogether in Isabelle-95!
  The new version of HOL (previously called CHOL) uses a curried
syntax for functions.
  Application looks like f a b instead of f(a,b).
Mutually recursive inductive definitions finally work in HOL.
  In ZF, pattern-matching on tuples is now available in all
abstractions.  It translates to the operator "split".  (Previously this
was only available in HOL.)

   Larry Paulson
   Tobias Nipkow