7 NEWS file in the distribution for more details. Some notable changes 
7 NEWS file in the distribution for more details. Some notable changes 
8 are: 
8 are: 
9 
9 
10 * Explicit proof terms for type class reasoning. 
10 * Explicit proof terms for type class reasoning. 
11 
11 
12 * Authentic syntax for *all* logical entities (type classes, type 
12 * Robust treatment of concrete syntax for different logical entities; 
13 constructors, term constants): provides simple and robust 
13 mixfix syntax in local proof context. 
14 correspondence between formal entities and concrete syntax. 

15 
14 
16 * HOL: Package for constructing quotient types. 
15 * Type declarations and notation within local theory context. 
17 
16 
18 * HOL: Code generation now with simple concept for abstract 
17 * HOL: package for quotient types. 
19 datatypes obeying invariants; applications for typical data structures 

20 (e.g. search trees) can be found in the library. 

21 
18 
22 * HOL: New development of the Reals using Cauchy Sequences. 
19 * HOL code generation: simple concept for abstract datatypes obeying 

20 invariants (e.g. redblack trees). 
23 
21 
24 * HOL: Reorganization of abstract algebra type class hierarchy. 
22 * HOL: new development of the Reals using Cauchy Sequences. 
25 
23 
26 * Commands 'types', 'typedecl' and 'typedef' now work within a local theory 
24 * HOL: reorganization of abstract algebra type class hierarchy. 
27 context  without introducing dependencies on parameters or 
25 
28 assumptions. 
26 * HOL: substantial reorganization of main library and related tools. 

27 

28 * HOLCF: reorganization of 'domain' package. 

29 
29 
30 
30 You may get Isabelle20092 from the following mirror sites: 
31 You may get Isabelle20092 from the following mirror sites: 
31 
32 
32 Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ 
33 Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ 
33 Munich (Germany) http://isabelle.in.tum.de/ 
34 Munich (Germany) http://isabelle.in.tum.de/ 