wenzelm@9928: 
wenzelm@12927: Subject: Announcing Isabelle2002
wenzelm@9928: To: isabelle-users@cl.cam.ac.uk
wenzelm@9928: 
wenzelm@12927: Isabelle2002 is now available.
wenzelm@12927: 
wenzelm@12995: This release provides major improvements.  The Isar language has
wenzelm@12995: reached a mature state; the core engine is able to record full proof
wenzelm@12995: terms; many aspects of the library have been reworked; several
wenzelm@12995: substantial case studies have been added.  Some changes may cause
wenzelm@12995: incompatibility with earlier versions, but improve accessibility of
wenzelm@12995: Isabelle for new users.
wenzelm@12927: 
wenzelm@12983: The most prominent highlights of Isabelle2002 are as follows (see the
wenzelm@12983: NEWS of the distribution for more details).
wenzelm@12964: 
wenzelm@12995:   * The Isabelle/HOL tutorial is to be published as LNCS 2283;
wenzelm@12983:     Isabelle2002 is the official version to go along with that book
wenzelm@12983:     (by Tobias Nipkow, Larry Paulson, Markus Wenzel).
wenzelm@12983: 
wenzelm@12983:   * Pure: explicit proof terms for all internal inferences:
wenzelm@12983:     object-logics, proof tools etc. will benefit automatically
wenzelm@12983:     (by Stefan Berghofer).
wenzelm@10161: 
wenzelm@12983:   * Pure/Isar: proper integration of the locale package for modular
wenzelm@12983:     theory development; additional support for rename/merge
wenzelm@12983:     operations, and type-inference for structured specifications
wenzelm@12983:     (by Markus Wenzel).
wenzelm@12983: 
wenzelm@12983:   * Pure/Isar: streamlined induction proof patterns
wenzelm@12983:     (by Markus Wenzel).
wenzelm@12983: 
wenzelm@12983:   * Pure/HOL: infrastructure for generating functional and relational
wenzelm@12983:     code, using the ML run-time environment (by Stefan Berghofer).
wenzelm@12983: 
paulson@12993:   * HOL/library: numerals on all number types; several
wenzelm@12983:     improvements of tuple and record types; new definite description
paulson@12993:     operator; keep Hilbert's epsilon (Axiom of Choice) out of basic theories.
wenzelm@12964: 
wenzelm@12983:   * HOL/Bali: large application concerning formal treatment of Java.
wenzelm@12983:     (by David von Oheimb and Norbert Schirmer).
wenzelm@12983: 
prensani@12996:   * HOL/HoareParallel: large application concerning verification of
prensani@12996:     parallel imperative programs (Owicki-Gries method, Rely-Guarantee
prensani@12996:     method, verification examples: garbage collection, mutual
prensani@12996:     exclusion, etc.)
wenzelm@12983:     (by Leonor Prensa Nieto).
wenzelm@12983: 
wenzelm@12983:   * HOL/GroupTheory: group theory examples including Sylow's theorem
wenzelm@12983:     (by Florian Kammüller).
wenzelm@9928: 
wenzelm@12983:   * HOL/IMP: new proofs in Isar format
wenzelm@12983:     (by Gerwin Klein).
wenzelm@12983: 
wenzelm@12983:   * ZF/UNITY: typeless version of Chandy and Misra's formalism
wenzelm@12983:     (by Sidi O Ehmety).
wenzelm@10162: 
wenzelm@12983:   * System: improvements and simplifications of document preparation
wenzelm@12983:     (by Markus Wenzel).
wenzelm@12983: 
wenzelm@12983:   * System: support for Poly/ML 4.1.1 and PolyML/4.1.2, admitting
wenzelm@12983:     larger heap size of applications.
wenzelm@12983: 
wenzelm@12983:   * System: support for MacOS X (for Poly/ML and SML/NJ).
wenzelm@12964: 
wenzelm@10166: 
wenzelm@12964: You may get Isabelle2002 from any of the following mirror sites:
wenzelm@9928: 
wenzelm@9928:   Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
wenzelm@9928:   Munich (Germany)  http://isabelle.in.tum.de/dist/
wenzelm@10161:   New Jersey (USA)  ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html
wenzelm@10161:   Stanford (USA)    ftp://rodin.stanford.edu/pub/smlnj/isabelle/index.html