replaced read_term_legacy by read_prop_legacy;
read: intern_skolem before type-inference (many workarounds!);
read: reject_tvars;
removed obsolete TypeInfer.logicT -- use dummyT;
add_fixes: not constraints for external names;
Subject: Announcing Isabelle2005
To: isabelle-users@cl.cam.ac.uk
Isabelle2005 is now available.
This release provides substantial advances over Isabelle2004, see the
first 1000 lines of NEWS in the distribution for more details. Some
highlights are:
* Interpretation of locale expressions in theories, locales, and proof
contexts.
* Substantial library improvements (HOL, HOL-Complex, HOLCF).
* Proof tools for transitivity reasoning.
* General 'find_theorems' command (by term patterns, as
intro/elim/simp rules etc.).
* Commands for generating ad-hoc draft documents.
* Support for Unicode proof documents (UTF-8).
* Major internal reorganizations and performance improvements.
You may get Isabelle2005 from the following mirror sites:
Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
Munich (Germany) http://isabelle.in.tum.de/
Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/