equal
deleted
inserted
replaced
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 Isabelle991 are as follows. 
14 The most prominent highlights of Isabelle991 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 HindleyMilner polymorphism for proof texts. 
21 o HindleyMilner 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 mathmode. 
23 fake mathmode. 
24 o Extended "Isabelle/Isar Reference Manual" 
24 o Extended "Isabelle/Isar Reference Manual" 
25 http://isabelle.in.tum.de/doc/isarref.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 