wenzelm@17544: Subject: Announcing Isabelle2005
wenzelm@9928: To: isabelle-users@cl.cam.ac.uk
wenzelm@9928: 
wenzelm@17544: Isabelle2005 is now available.
wenzelm@17544: 
wenzelm@17572: This release provides substantial advances over Isabelle2004, see the
wenzelm@17572: first 1000 lines of NEWS in the distribution for more details.  Some
wenzelm@17692: highlights are:
wenzelm@17544: 
wenzelm@17544: * Interpretation of locale expressions in theories, locales, and proof
wenzelm@17544: contexts.
wenzelm@17544: 
wenzelm@17544: * Substantial library improvements (HOL, HOL-Complex, HOLCF).
wenzelm@12927: 
wenzelm@17544: * Proof tools for transitivity reasoning.
wenzelm@17544: 
wenzelm@17544: * General 'find_theorems' command (by term patterns, as
wenzelm@17544: intro/elim/simp rules etc.).
wenzelm@17544: 
wenzelm@17692: * Commands for generating ad-hoc draft documents.
wenzelm@17544: 
wenzelm@17544: * Support for Unicode proof documents (UTF-8).
wenzelm@17544: 
wenzelm@17544: * Major internal reorganizations and performance improvements.
wenzelm@12927: 
wenzelm@12983: 
wenzelm@17544: You may get Isabelle2005 from the following mirror sites:
wenzelm@9928: 
haftmann@17696:   Cambridge (UK)       http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
haftmann@17696:   Munich (Germany)     http://isabelle.in.tum.de/
kleing@14616:   Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/