ANNOUNCE
author wenzelm
Fri Oct 06 16:11:53 2000 +0200 (2000-10-06)
changeset 10162 947b7b8b0a69
parent 10161 4a3cd038aff8
child 10165 eb69823db997
permissions -rw-r--r--
tuned;
     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, including the 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.
    15 
    16   * Isabelle/Isar improvements (Markus Wenzel)
    17       o Support of tactic-emulation scripts for easy porting of legacy ML
    18         scripts (see also the HOL/Lambda example).
    19       o Better support for scalable verification tasks (manage large
    20         contexts in induction, generalized existence reasoning etc.)
    21       o Hindley-Milner polymorphism for proof texts.
    22       o More robust document preparation, better LaTeX output due to
    23         fake math-mode.
    24       o Extended "Isabelle/Isar Reference Manual"
    25         http://isabelle.in.tum.de/doc/isar-ref.pdf
    26 
    27   * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and
    28     Cornelia Pusch)
    29     Formalization of a fragment of Java, together with a corresponding
    30     virtual machine and a specification of its bytecode verifier and a
    31     lightweight bytecode verifier, including proofs of type-safety.
    32 
    33   * HOL/BCV (Tobias Nipkow)
    34     Generic model of bytecode verification, i.e. data-flow
    35     analysis for assembly languages with subtypes.
    36 
    37   * HOL/Real (Jacques Fleuriot)
    38     More on nonstandard real analysis.
    39 
    40   * HOL/Algebra (Clemens Ballarin)
    41     Rings and univariate polynomials.
    42 
    43   * HOL/NumberTheory (Thomas Rasmussen)
    44     Fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
    45     Fermat/Euler Theorem, Wilson's Theorem.
    46 
    47   * HOL/Lambda (Stefan Berghofer and Tobias Nipkow)
    48     More on termination of simply-typed lambda-terms; converted into
    49     an Isabelle/Isar tactic emulation script.
    50 
    51   * HOL/Lattice (Markus Wenzel)
    52     Lattices and orders in Isabelle/Isar.
    53 
    54   * HOL/Isar_examples (Markus Wenzel)
    55     More examples, including a formulation of Hoare Logic in Isabelle/Isar.
    56 
    57   * HOL/Prolog (David von Oheimb)
    58     A (bare-bones) implementation of Lambda-Prolog.
    59 
    60 See the NEWS file distributed with Isabelle for more details.
    61 
    62 
    63 You may get Isabelle99-1 from any of the following mirror sites:
    64 
    65   Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
    66   Munich (Germany)  http://isabelle.in.tum.de/dist/
    67   New Jersey (USA)  ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html
    68   Stanford (USA)    ftp://rodin.stanford.edu/pub/smlnj/isabelle/index.html