Projects / Isabelle / Releases

RSS All releases of Isabelle

  •  21 Mar 2006 14:00

Release Notes: This release contains major enhancements in specification elements, the user interface, and proof tools. The most notable additions on the theorem proving and specification side are interpretation of locale expressions in theories, locales, and proof contexts, substantial library improvements, proof tools for transitivity reasoning, and performance improvements. On the user interface side, this release contains a new, general find-theorems command (by term patterns, as intro/elim/simp rules etc.), new commands for generating adhoc draft documents, and support for Unicode proof documents.

  •  01 May 2004 06:53

Release Notes: The library of the HOL4 system (about 2,500 additional theorems) has been imported. Theories for rational numbers, rings, and matrices have been added, as well as over 250 basic numerical laws for semirings, rings, and fields. Handling of linear and partial orders has been improved. Two commands to search for counterexamples have been added. Presentation and x-symbol handling has been improved.

  •  19 Jun 2003 12:24

Release Notes: This release has a new framework for extracting programs from constructive proofs in HOL, full Presburger arithmetic, locales (named proof contexts), and an improved simplifier. Library additions include HOL/Algebra (proofs in classical algebra), HOL/Complex (complex numbers with numeric constants and some complex analysis, including nonstandard analysis), HOL/NumberTheory (Gauss's law of quadratic reciprocity), and ZF/Constructible (Gödel's proof of the relative consistency of the axiom of choice).

  •  11 Mar 2002 15:07

Release Notes: The Isabelle/HOL tutorial is to be published as book (LNCS volume 2283). Isabelle now supports explicit proof terms, a better locale package, and an ML code generator for functional and relational specifications. The document preparation tools have been simplified. Poly/ML 4.1.1 and 4.1.2 are supported. MacOS X support has been improved. Library additions include: Bali (formal treatment of Java), HoareParallel (verification of parallel imperative programs), group theory examples including Sylow's theorem, and a typeless version of Chandy and Misra's formalism (ZF/UNITY).

  •  16 Feb 2001 08:39

Release Notes: This release includes several improvements to document preparation (antiquotations, improved style files, and sub/super scripts), improvements to the Isar proof language (better obtain, better induct, and a conversion script for legacy ML files), improvements to HOL (small structural changes, better arithmetic for reals), improvements to the simplifier (implemented a derived rule), and support for Poly/ML 4.0.

  •  30 Jan 2001 06:13

    Release Notes: Initial freshmeat announcement.


    Project Spotlight


    A professional Web Content Management System.


    Project Spotlight


    A tool that makes normal maps for 2D art.