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