Projects / Isabelle / Releases

All releases of Isabelle

  •  21 Mar 2006 22:00
Avatar

    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 13:53
    Avatar

      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 19:24
      Avatar

        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 20:07
        Avatar

          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 13:39
          Avatar

            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.

            •  10 Oct 2000 16:19
            Avatar

              Release Notes: Initial freshmeat announcement.

              Screenshot

              Project Spotlight

              episoder

              A tool to tell you about new episodes of your favourite TV shows.

              Screenshot

              Project Spotlight

              BalanceNG

              A modern software IP load balancer.