ANNOUNCE
changeset 11062 e86340dc1d28
parent 10168 50be659d4222
child 11108 43791f99d71e
equal deleted inserted replaced
11061:9b9d48ce3b6c 11062:e86340dc1d28
     1 
     1 
     2 Subject: Announcing Isabelle99-1
     2 Subject: Announcing Isabelle99-2
     3 To: isabelle-users@cl.cam.ac.uk
     3 To: isabelle-users@cl.cam.ac.uk
     4 
     4 
     5 Isabelle99-1 is now available.  This release continues the line of
     5 Isabelle99-2 is now available.  This release continues the line of
     6 Isabelle99, introducing numerous improvements, both internal and user
     6 Isabelle99, introducing various improvements in robustness and
     7 visible.
     7 usability.
     8 
     8 
     9 In particular, great care has been taken to improve robustness and
     9 The most prominent highlights of Isabelle99-2 are as follows.  See the
    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.
    10 NEWS file distributed with Isabelle for more details.
    16 
    11 
    17   * Isabelle/Isar improvements (Markus Wenzel)
    12   * Poly/ML 4.0 used by default
    18       o Support of tactic-emulation scripts for easy porting of legacy ML
    13     More robust, less disk space required.
    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 
    14 
    27   * HOL/Algebra (Clemens Ballarin)
    15   * Pure/Simplifier (Stefan Berghofer)
    28     Rings and univariate polynomials.
    16     Proper implementation as a derived rule, outside the kernel!
    29 
    17 
    30   * HOL/BCV (Tobias Nipkow)
    18   * Isabelle/Isar (Markus Wenzel)
    31     Generic model of bytecode verification.
    19     Numerous usability improvements, e.g. support for initial
       
    20     schematic goals, failure prediction of subgoal statements,
       
    21     handling of non-atomic statements in induction.
    32 
    22 
    33   * HOL/IMPP (David von Oheimb)
    23   * Improved document preparation (Markus Wenzel)
    34     Extension of IMP with local variables and mutually recursive procedures.
    24     Near math-mode, sub/super scripts, more symbols etc.
    35 
    25 
    36   * HOL/Isar_examples (Markus Wenzel)
    26   * HOL/Library (Gertrud Bauer, Tobias Nipkow, Lawrence C Paulson,
    37     More examples, including a formulation of Hoare Logic in Isabelle/Isar.
    27       Thomas M Rasmussen, Markus Wenzel)
       
    28     A collection of generic theories to be used together with main HOL.
    38 
    29 
    39   * HOL/Lambda (Stefan Berghofer and Tobias Nipkow)
    30   * HOL/Real and HOL/Hyperreal (Lawrence C Paulson and Jacques Fleuriot)
    40     More on termination of simply-typed lambda-terms (Isar script).
    31     General cleanup, more on nonstandard real analysis.
    41 
    32 
    42   * HOL/Lattice (Markus Wenzel)
    33   * HOL/Unix (Markus Wenzel)
    43     Lattices and orders in Isabelle/Isar.
    34     Some Aspects of Unix file-system security; demonstrates
       
    35     Isabelle/Isar in typical system modelling and verification tasks.
    44 
    36 
    45   * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and
    37   * HOL/Tutorial (Tobias Nipkow, Lawrence C Paulson)
    46     Cornelia Pusch)
    38     Extended version of the Isabelle/HOL tutorial.
    47     Formalization of a fragment of Java, together with a corresponding
       
    48     virtual machine and a specification of its bytecode verifier.
       
    49 
    39 
    50   * HOL/NumberTheory (Thomas Rasmussen)
    40 You may get Isabelle99-2 from any of the following mirror sites:
    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 
    41 
    62   Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
    42   Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
    63   Munich (Germany)  http://isabelle.in.tum.de/dist/
    43   Munich (Germany)  http://isabelle.in.tum.de/dist/
    64   New Jersey (USA)  ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html
    44   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
    45   Stanford (USA)    ftp://rodin.stanford.edu/pub/smlnj/isabelle/index.html