ANNOUNCE

* HOL-Word:
New extensive library and type for generic, fixed size machine
words, with arithemtic, bit-wise, shifting and rotating operations,
reflection into int, nat, and bool lists, automation for linear
arithmetic (by automatic reflection into nat or int), including
lemmas on overflow and monotonicity. Instantiated to all appropriate
arithmetic type classes, supporting automatic simplification of
numerals on all operations. Jointly developed by NICTA, Galois, and
PSU.

* still to do: README.html/document + moving some of the generic lemmas
to appropriate place in distribution

Subject: Announcing Isabelle2005
To: [e-mail]

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/