1 Subject: Announcing Isabelle2004 
1 Subject: Announcing Isabelle2005 
2 To: isabelleusers@cl.cam.ac.uk 
2 To: isabelleusers@cl.cam.ac.uk 
3 
3 
4 Isabelle2004 is now available. 
4 Isabelle2005 is now available. 
5 
5 
6 This release provides many improvements and a few substantial advances over 
6 This release provides substantial advances over Isabelle2004. Some 
7 Isabelle2003. The most prominent highlights of Isabelle2004 are as follows 
7 highlights are as follows (see the NEWS of the distribution for more 
8 (see the NEWS of the distribution for more details): 
8 details): 

9 

10 * Interpretation of locale expressions in theories, locales, and proof 

11 contexts. 

12 

13 * Substantial library improvements (HOL, HOLComplex, HOLCF). 

14 

15 * Proof tools for transitivity reasoning. 

16 

17 * General 'find_theorems' command (by term patterns, as 

18 intro/elim/simp rules etc.). 

19 

20 * Commands for generating adhoc draft documents. 

21 

22 * Support for Unicode proof documents (UTF8). 

23 

24 * Major internal reorganizations and performance improvements. 
9 
25 
10 
26 
11 * New image HOL4 with imported library from HOL4 system on top of 
27 You may get Isabelle2005 from the following mirror sites: 
12 HOLComplex (about 2500 additional theorems). 

13 

14 * New theory Ring_and_Field with over 250 basic numerical laws, 

15 all proved in axiomatic type classes for semirings, rings and fields. 

16 

17 * Type "rat" of the rational numbers available in HOLComplex. 

18 

19 * New locale "ring" for noncommutative rings in HOLAlgebra. 

20 

21 * New theory of matrices with an application to linear programming in 

22 HOLMatrix. 

23 

24 * Improved locales (named proof contexts), instantiation of locales. 

25 

26 * Improved handling of linear and partial orders in simplifier. 

27 

28 * New "specification" command for definition by specification. 

29 

30 * New Isar command "finalconsts" prevents constants being given a definition 

31 later. 

32 

33 * Command "arith" now generates counterexamples for reals as well. 

34 

35 * New "quickcheck" command to search for counterexamples of executable goals. 

36 (see HOL/ex/Quickcheck_Examples.thy) 

37 

38 * New "refute" command to search for finite countermodels of goals. 

39 (see HOL/ex/Refute_Examples.thy) 

40 

41 * Presentation and xsymbol enhancements, greek letters and sub/superscripts 

42 allowed in identifiers. 

43 

44 

45 You may get Isabelle2004 from the following mirror sites: 

46 
28 
47 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/ 
29 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/ 
48 Munich (Germany) http://isabelle.in.tum.de/dist/ 
30 Munich (Germany) http://isabelle.in.tum.de/dist/ 
49 Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/ 
31 Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/ 
50 

51 Gerwin Klein 

52 Tobias Nipkow 

53 Larry Paulson 
