- 'induct' may now use elim-style induction rules without chaining
facts, using ``missing'' premises from the goal state; this allows
rules stemming from inductive sets to be applied in unstructured
scripts, while still benefitting from proper handling of non-atomic
statements; NB: major inductive premises need to be put first, all the
rest of the goal is passed through the induction;
Subject: Announcing Isabelle2001
To: isabelle-users@cl.cam.ac.uk
Isabelle2001 is now available.
The most prominent highlights of Isabelle2001 are as follows. See the
NEWS file distributed with Isabelle for more details.
* Specific support for Poly/ML 4.1.1
Faster, manages large heaps.
* Meta-level proof terms (Stefan Berghofer)
You may get Isabelle2001 from any of the following mirror sites:
Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
Munich (Germany) http://isabelle.in.tum.de/dist/
New Jersey (USA) ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html
Stanford (USA) ftp://rodin.stanford.edu/pub/smlnj/isabelle/index.html