ANNOUNCE
changeset 10165 eb69823db997
parent 10162 947b7b8b0a69
child 10166 fb99cee36240
equal deleted inserted replaced
10164:c240747082aa 10165:eb69823db997
     6 Isabelle99, introducing numerous improvements, both internal and user
     6 Isabelle99, introducing numerous improvements, both internal and user
     7 visible.
     7 visible.
     8 
     8 
     9 In particular, great care has been taken to improve robustness and
     9 In particular, great care has been taken to improve robustness and
    10 ease use and installation of the complete Isabelle working
    10 ease use and installation of the complete Isabelle working
    11 environment, including the Proof General user interface support, WWW
    11 environment.  This includes Proof General user interface support, WWW
    12 presentation of theories and the Isabelle document preparation system.
    12 presentation of theories and the Isabelle document preparation system.
    13 
    13 
    14 The most prominent highlights of Isabelle99-1 are as follows.
    14 The most prominent highlights of Isabelle99-1 are as follows.
    15 
    15 
    16   * Isabelle/Isar improvements (Markus Wenzel)
    16   * Isabelle/Isar improvements (Markus Wenzel)
    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         http://isabelle.in.tum.de/doc/isar-ref.pdf
       
    26 
    25 
    27   * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and
    26   * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and
    28     Cornelia Pusch)
    27     Cornelia Pusch)
    29     Formalization of a fragment of Java, together with a corresponding
    28     Formalization of a fragment of Java, together with a corresponding
    30     virtual machine and a specification of its bytecode verifier and a
    29     virtual machine and a specification of its bytecode verifier and a