16 
16 
17 * The Isabelle/HOL tutorial is to be published as LNCS 2283; 
17 * The Isabelle/HOL tutorial is to be published as LNCS 2283; 
18 Isabelle2002 is the official version to go along with that book 
18 Isabelle2002 is the official version to go along with that book 
19 (by Tobias Nipkow, Larry Paulson, Markus Wenzel). 
19 (by Tobias Nipkow, Larry Paulson, Markus Wenzel). 
20 
20 
21 * Pure: explicit proof terms for all internal inferences: 
21 * Pure: explicit proof terms for all internal inferences; 
22 objectlogics, proof tools etc. will benefit automatically 
22 objectlogics, proof tools etc. will benefit automatically 
23 (by Stefan Berghofer). 
23 (by Stefan Berghofer). 
24 
24 
25 * Pure/Isar: proper integration of the locale package for modular 
25 * Pure/Isar: proper integration of the locale package for modular 
26 theory development; additional support for rename/merge 
26 theory development; additional support for rename/merge 
27 operations, and typeinference for structured specifications 
27 operations, and typeinference for structured specifications 
28 (by Markus Wenzel). 
28 (by Markus Wenzel). 
29 
29 
30 * Pure/Isar: streamlined induction proof patterns 
30 * Pure/Isar: streamlined cases/induction proof patterns 
31 (by Markus Wenzel). 
31 (by Markus Wenzel). 
32 
32 
33 * Pure/HOL: infrastructure for generating functional and relational 
33 * Pure/HOL: infrastructure for generating functional and relational 
34 code, using the ML runtime environment (by Stefan Berghofer). 
34 code, using the ML runtime environment 

35 (by Stefan Berghofer). 
35 
36 
36 * HOL/library: numerals on all number types; several 
37 * HOL/library: numerals on all number types; several improvements of 
37 improvements of tuple and record types; new definite description 
38 tuple and record types; new definite description operator; keep 
38 operator; keep Hilbert's epsilon (Axiom of Choice) out of basic theories. 
39 Hilbert's epsilon (Axiom of Choice) out of basic theories 

40 (by Stefan Berghofer, Larry Paulson, Markus Wenzel). 
39 
41 
40 * HOL/Bali: large application concerning formal treatment of Java. 
42 * HOL/Bali: large application concerning formal treatment of Java. 
41 (by David von Oheimb and Norbert Schirmer). 
43 (by David von Oheimb and Norbert Schirmer). 
42 
44 
43 * HOL/HoareParallel: large application concerning verification of 
45 * HOL/HoareParallel: large application concerning verification of 
44 parallel imperative programs (OwickiGries method, RelyGuarantee 
46 parallel imperative programs (OwickiGries method, RelyGuarantee 
45 method, examples of garbage collection, mutual exclusion, etc.) 
47 method, examples of garbage collection, mutual exclusion) 
46 (by Leonor Prensa Nieto). 
48 (by Leonor Prensa Nieto). 
47 
49 
48 * HOL/GroupTheory: group theory examples including Sylow's theorem 
50 * HOL/GroupTheory: group theory examples including Sylow's theorem 
49 (by Florian Kammüller). 
51 (by Florian Kammueller). 
50 
52 
51 * HOL/IMP: new proofs in Isar format 
53 * HOL/IMP: several new proofs in Isar format 
52 (by Gerwin Klein). 
54 (by Gerwin Klein). 
53 
55 
54 * HOL/MicroJava: exception handling on the bytecode level 
56 * HOL/MicroJava: exception handling on the bytecode level 
55 (by Gerwin Klein). 
57 (by Gerwin Klein). 
56 
58 
59 
61 
60 * System: improvements and simplifications of document preparation 
62 * System: improvements and simplifications of document preparation 
61 (by Markus Wenzel). 
63 (by Markus Wenzel). 
62 
64 
63 * System: support for Poly/ML 4.1.1 and PolyML/4.1.2, admitting 
65 * System: support for Poly/ML 4.1.1 and PolyML/4.1.2, admitting 
64 larger heap size of applications. 
66 larger heap size of applications; support for MacOS X (Poly/ML and 
65 
67 SML/NJ). 
66 * System: support for MacOS X (for Poly/ML and SML/NJ). 

67 

68 
68 
69 You may get Isabelle2002 from any of the following mirror sites: 
69 You may get Isabelle2002 from any of the following mirror sites: 
70 
70 
71 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/ 
71 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/ 
72 Munich (Germany) http://isabelle.in.tum.de/dist/ 
72 Munich (Germany) http://isabelle.in.tum.de/dist/ 