[T1] ================================================ AMAST Links 02 05

                         Isabelle 94 Release 3

   *Update* of information in [AL0202T4].

  A new update of Isabelle, Isabelle94-3, is now available on the 
_Cambridge ftp site_ at URL:

   ftp://ftp.cl.cam.ac.uk 

in the file /ml/Isabelle94-3.tar.gz.  It is also at the Munich site.

  Here is a summary of the changes from Isabelle94-2.
 o  There is a new infix operator, addss, allowing the classical 
    reasoner to perform simplification at each step of its search.
    For example, _fast-tac (cs addss ss)_.
      This still performs depth-first search, and so differs from using
    setsolver to make the simlifier call the classical reasoner.

 o  There is a new logic called CHOL. It is the same as HOL, but with
    a curried syntax from functions.  Application looks like _f a b_ 
    instead of _f(a,b)_.  Also pairs look like _(a,b)_ instead of 
    _<a,b>_.  *Please Note:* CHOL will replace HOL in Isabelle95! 
      In CHOL, pattern matching on tuples is now available in all 
    abstractions.  It translates to proper _split_.  A new theory of 
    integers is available.

 o  In ZF, integer numerals now denote two's-complement binary 
    integers.  Arithmetic operations can be performed by rewriting.
    See ZF/ex/Bin.ML.

 o  There are many new examples: I/O automata, Church-Rosser theorem,
    equivalents of the axiom of choice.

  Thanks to everyone who provided theories or examples. Their names are
acknowledged on the individual files.

  Larry Paulson