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 notable features 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 adhoc draft documents. * Support for Unicode proof documents (UTF-8). * Major internal reorganizations and performance improvements. * 'defs': more checks for overloading, but less checks for cyclic dependencies! 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/