ANNOUNCE
author wenzelm
Fri Oct 06 17:35:58 2000 +0200 (2000-10-06)
changeset 10168 50be659d4222
parent 10167 4ede3a80e5e5
child 11062 e86340dc1d28
permissions -rw-r--r--
final tuning;
     1 
     2 Subject: Announcing Isabelle99-1
     3 To: isabelle-users@cl.cam.ac.uk
     4 
     5 Isabelle99-1 is now available.  This release continues the line of
     6 Isabelle99, introducing numerous improvements, both internal and user
     7 visible.
     8 
     9 In particular, great care has been taken to improve robustness and
    10 ease use and installation of the complete Isabelle working
    11 environment.  This includes Proof General user interface support, WWW
    12 presentation of theories and the Isabelle document preparation system.
    13 
    14 The most prominent highlights of Isabelle99-1 are as follows.  See the
    15 NEWS file distributed with Isabelle for more details.
    16 
    17   * Isabelle/Isar improvements (Markus Wenzel)
    18       o Support of tactic-emulation scripts for easy porting of legacy ML
    19         scripts (see also the HOL/Lambda example).
    20       o Better support for scalable verification tasks (manage large
    21         contexts in induction, generalized existence reasoning etc.)
    22       o Hindley-Milner polymorphism for proof texts.
    23       o More robust document preparation, better LaTeX output due to
    24         fake math-mode.
    25       o Extended "Isabelle/Isar Reference Manual".
    26 
    27   * HOL/Algebra (Clemens Ballarin)
    28     Rings and univariate polynomials.
    29 
    30   * HOL/BCV (Tobias Nipkow)
    31     Generic model of bytecode verification.
    32 
    33   * HOL/IMPP (David von Oheimb)
    34     Extension of IMP with local variables and mutually recursive procedures.
    35 
    36   * HOL/Isar_examples (Markus Wenzel)
    37     More examples, including a formulation of Hoare Logic in Isabelle/Isar.
    38 
    39   * HOL/Lambda (Stefan Berghofer and Tobias Nipkow)
    40     More on termination of simply-typed lambda-terms (Isar script).
    41 
    42   * HOL/Lattice (Markus Wenzel)
    43     Lattices and orders in Isabelle/Isar.
    44 
    45   * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and
    46     Cornelia Pusch)
    47     Formalization of a fragment of Java, together with a corresponding
    48     virtual machine and a specification of its bytecode verifier.
    49 
    50   * HOL/NumberTheory (Thomas Rasmussen)
    51     Fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
    52     Fermat/Euler Theorem, Wilson's Theorem.
    53 
    54   * HOL/Prolog (David von Oheimb)
    55     A (bare-bones) implementation of Lambda-Prolog.
    56 
    57   * HOL/Real (Jacques Fleuriot)
    58     More on nonstandard real analysis.
    59 
    60 You may get Isabelle99-1 from any of the following mirror sites:
    61 
    62   Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
    63   Munich (Germany)  http://isabelle.in.tum.de/dist/
    64   New Jersey (USA)  ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html
    65   Stanford (USA)    ftp://rodin.stanford.edu/pub/smlnj/isabelle/index.html