author berghofe
Mon, 23 Oct 2006 00:47:25 +0200
changeset 21085 3cb13b06ad72
parent 17696 eccdee8a0790
child 24802 6bd8ec8f3fc8
permissions -rw-r--r--
Added Compile and Height examples to Nominal directory.

Subject: Announcing Isabelle2005

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

* 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)
  Munich (Germany)
  Sydney (Australia)