Isabelle 94 Release 3
Update of information in
[AL0202T4]
.
A new update of Isabelle, Isabelle94-3, is now available on the
Cambridge ftp site
.
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.
-
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.
-
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.
-
In ZF, integer numerals now denote two's-complement binary
integers. Arithmetic operations can be performed by rewriting.
See ZF/ex/Bin.ML.
-
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