equal
deleted
inserted
replaced
5 
5 
6 This release improves upon Isabelle20091 in many respects, see the 
6 This release improves upon Isabelle20091 in many respects, see the 
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 * FIXME 
10 * Explicit proof terms for type class reasoning. 
11 
11 

12 * Authentic syntax for *all* logical entities (type classes, type 

13 constructors, term constants): provides simple and robust 

14 correspondence between formal entities and concrete syntax. 

15 

16 * HOL: Package for constructing quotient types. 

17 

18 * HOL: Code generation now with simple concept for abstract 

19 datatypes obeying invariants; applications for typical data structures 

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

21 

22 * HOL: New development of the Reals using Cauchy Sequences. 

23 

24 * HOL: Reorganization of abstract algebra type class hierarchy. 

25 

26 * Commands 'types', 'typedecl' and 'typedef' now work within a local theory 

27 context  without introducing dependencies on parameters or 

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