author wenzelm
Fri, 06 Oct 2000 17:21:46 +0200
changeset 10166 fb99cee36240
parent 10165 eb69823db997
child 10167 4ede3a80e5e5
permissions -rw-r--r--

Subject: Announcing Isabelle99-1

Isabelle99-1 is now available.  This release continues the line of
Isabelle99, introducing numerous improvements, both internal and user

In particular, great care has been taken to improve robustness and
ease use and installation of the complete Isabelle working
environment.  This includes Proof General user interface support, WWW
presentation of theories and the Isabelle document preparation system.

The most prominent highlights of Isabelle99-1 are as follows.

  * Isabelle/Isar improvements (Markus Wenzel)
      o Support of tactic-emulation scripts for easy porting of legacy ML
        scripts (see also the HOL/Lambda example).
      o Better support for scalable verification tasks (manage large
        contexts in induction, generalized existence reasoning etc.)
      o Hindley-Milner polymorphism for proof texts.
      o More robust document preparation, better LaTeX output due to
        fake math-mode.
      o Extended "Isabelle/Isar Reference Manual".

  * HOL/Algebra (Clemens Ballarin)
    Rings and univariate polynomials.

  * HOL/BCV (Tobias Nipkow)
    Generic model of bytecode verification, i.e. data-flow
    analysis for assembly languages with subtypes.

  * HOL/IMPP (David von Oheimb)
    Extension of IMP with local variables and mutually recursive

  * HOL/Isar_examples (Markus Wenzel)
    More examples, including a formulation of Hoare Logic in Isabelle/Isar.

  * HOL/Lambda (Stefan Berghofer and Tobias Nipkow)
    More on termination of simply-typed lambda-terms; converted into
    an Isabelle/Isar tactic emulation script.

  * HOL/Lattice (Markus Wenzel)
    Lattices and orders in Isabelle/Isar.

  * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and
    Cornelia Pusch)
    Formalization of a fragment of Java, together with a corresponding
    virtual machine and a specification of its bytecode verifier and a
    lightweight bytecode verifier, including proofs of type-safety.

  * HOL/NumberTheory (Thomas Rasmussen)
    Fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
    Fermat/Euler Theorem, Wilson's Theorem.

  * HOL/Real (Jacques Fleuriot)
    More on nonstandard real analysis.

  * HOL/Prolog (David von Oheimb)
    A (bare-bones) implementation of Lambda-Prolog.

See the NEWS file distributed with Isabelle for more details.

You may get Isabelle99-1 from any of the following mirror sites:

  Cambridge (UK)
  Munich (Germany)
  New Jersey (USA)
  Stanford (USA)