ANNOUNCE
changeset 10166 fb99cee36240
parent 10165 eb69823db997
child 10167 4ede3a80e5e5
equal deleted inserted replaced
10165:eb69823db997 10166:fb99cee36240
    19       o Better support for scalable verification tasks (manage large
    19       o Better support for scalable verification tasks (manage large
    20         contexts in induction, generalized existence reasoning etc.)
    20         contexts in induction, generalized existence reasoning etc.)
    21       o Hindley-Milner polymorphism for proof texts.
    21       o Hindley-Milner polymorphism for proof texts.
    22       o More robust document preparation, better LaTeX output due to
    22       o More robust document preparation, better LaTeX output due to
    23         fake math-mode.
    23         fake math-mode.
    24       o Extended "Isabelle/Isar Reference Manual"
    24       o Extended "Isabelle/Isar Reference Manual".
    25 
    25 
    26   * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and
    26   * HOL/Algebra (Clemens Ballarin)
    27     Cornelia Pusch)
    27     Rings and univariate polynomials.
    28     Formalization of a fragment of Java, together with a corresponding
       
    29     virtual machine and a specification of its bytecode verifier and a
       
    30     lightweight bytecode verifier, including proofs of type-safety.
       
    31 
    28 
    32   * HOL/BCV (Tobias Nipkow)
    29   * HOL/BCV (Tobias Nipkow)
    33     Generic model of bytecode verification, i.e. data-flow
    30     Generic model of bytecode verification, i.e. data-flow
    34     analysis for assembly languages with subtypes.
    31     analysis for assembly languages with subtypes.
    35 
    32 
    36   * HOL/Real (Jacques Fleuriot)
    33   * HOL/IMPP (David von Oheimb)
    37     More on nonstandard real analysis.
    34     Extension of IMP with local variables and mutually recursive
       
    35     procedures.
    38 
    36 
    39   * HOL/Algebra (Clemens Ballarin)
    37   * HOL/Isar_examples (Markus Wenzel)
    40     Rings and univariate polynomials.
    38     More examples, including a formulation of Hoare Logic in Isabelle/Isar.
    41 
       
    42   * HOL/NumberTheory (Thomas Rasmussen)
       
    43     Fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
       
    44     Fermat/Euler Theorem, Wilson's Theorem.
       
    45 
    39 
    46   * HOL/Lambda (Stefan Berghofer and Tobias Nipkow)
    40   * HOL/Lambda (Stefan Berghofer and Tobias Nipkow)
    47     More on termination of simply-typed lambda-terms; converted into
    41     More on termination of simply-typed lambda-terms; converted into
    48     an Isabelle/Isar tactic emulation script.
    42     an Isabelle/Isar tactic emulation script.
    49 
    43 
    50   * HOL/Lattice (Markus Wenzel)
    44   * HOL/Lattice (Markus Wenzel)
    51     Lattices and orders in Isabelle/Isar.
    45     Lattices and orders in Isabelle/Isar.
    52 
    46 
    53   * HOL/Isar_examples (Markus Wenzel)
    47   * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and
    54     More examples, including a formulation of Hoare Logic in Isabelle/Isar.
    48     Cornelia Pusch)
       
    49     Formalization of a fragment of Java, together with a corresponding
       
    50     virtual machine and a specification of its bytecode verifier and a
       
    51     lightweight bytecode verifier, including proofs of type-safety.
       
    52 
       
    53   * HOL/NumberTheory (Thomas Rasmussen)
       
    54     Fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
       
    55     Fermat/Euler Theorem, Wilson's Theorem.
       
    56 
       
    57   * HOL/Real (Jacques Fleuriot)
       
    58     More on nonstandard real analysis.
    55 
    59 
    56   * HOL/Prolog (David von Oheimb)
    60   * HOL/Prolog (David von Oheimb)
    57     A (bare-bones) implementation of Lambda-Prolog.
    61     A (bare-bones) implementation of Lambda-Prolog.
       
    62 
       
    63 
    58 
    64 
    59 See the NEWS file distributed with Isabelle for more details.
    65 See the NEWS file distributed with Isabelle for more details.
    60 
    66 
    61 
    67 
    62 You may get Isabelle99-1 from any of the following mirror sites:
    68 You may get Isabelle99-1 from any of the following mirror sites: