ANNOUNCE
author paulson
Wed, 21 Sep 2005 18:35:19 +0200
changeset 17568 e93f7510e1e1
parent 17544 929d157d4369
child 17572 81fcc0029761
permissions -rw-r--r--
trying to limit the looping

Subject: Announcing Isabelle2005
To: isabelle-users@cl.cam.ac.uk

Isabelle2005 is now available.

This release provides substantial advances over Isabelle2004.  Some
highlights are as follows (see the NEWS of the distribution for more
details):

* 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 adhoc 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/dist/
  Munich (Germany)     http://isabelle.in.tum.de/dist/
  Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/