nipkow@14021

1 
Subject: Announcing Isabelle2003

wenzelm@9928

2 
To: isabelleusers@cl.cam.ac.uk

wenzelm@9928

3 

nipkow@14021

4 
Isabelle2003 is now available.

wenzelm@12927

5 

nipkow@14021

6 
This release provides many improvements and a few substantial advances over

nipkow@14021

7 
Isabelle2002. The most prominent highlights of Isabelle2003 are as follows

nipkow@14021

8 
(see the NEWS of the distribution for more details):

wenzelm@12927

9 

nipkow@14021

10 
* New framework for extracting programs from constructive proofs in HOL.

nipkow@14021

11 
(Berghofer)

wenzelm@12983

12 

nipkow@14021

13 
* Improved simplifier. The premises of a goal are completely

nipkow@14021

14 
interreduced, ie simplified wrt each other. (Berghofer)

wenzelm@10161

15 

nipkow@14021

16 
* Presburger arithmetic. Method arith can deal with quantified formulae over

nipkow@14021

17 
nat and int, and with mod, div and dvd wrt a numeral. (Chaieb and Nipkow)

wenzelm@12983

18 

nipkow@14021

19 
* New command to find all rules whose conclusion matches the current goal.

wenzelm@12983

20 

nipkow@14021

21 
* New command to trace why unification failed.

wenzelm@12983

22 

nipkow@14021

23 
* Locales (named proof contexts). The new implementation is fully

nipkow@14021

24 
integrated with Isar's notion of proof context, and locale specifications

nipkow@14021

25 
produce predicate definitions that allow to work with locales in more

nipkow@14021

26 
flexible ways. (Wenzel)

wenzelm@12983

27 

nipkow@14021

28 
* HOL/Algebra: proofs in classical algebra. Intended as a base for all

nipkow@14021

29 
algebraic developments in HOL. Currently covers group and ring theory.

nipkow@14021

30 
(Ballarin, Kammüller, Paulson)

wenzelm@9928

31 

nipkow@14021

32 
* HOL/Complex defines the type "complex" of the complex numbers, with numeric

nipkow@14021

33 
constants and some complex analysis, including nonstandard analysis. The

nipkow@14021

34 
image HOLComplex should be used for developments involving the real

nipkow@14021

35 
numbers too. Gauge integration and hyperreal logarithms have recently

nipkow@14021

36 
been added. (Fleuriot)

wenzelm@10162

37 

nipkow@14021

38 
* HOL/NumberTheory: added Gauss's law of quadratic reciprocity. (Avigad,

nipkow@14021

39 
Gray and Kramer)

wenzelm@12983

40 

nipkow@14021

41 
* ZF/Constructible: Gödel's proof of the relative consistency of the axiom

paulson@14022

42 
of choice is mechanized using Isabelle/ZF, following Kunen's wellknown

nipkow@14021

43 
textbook "Set Theory". (Paulson)

wenzelm@10166

44 

paulson@14022

45 
You may get Isabelle2003 from the following mirror sites:

wenzelm@9928

46 

wenzelm@9928

47 
Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/

wenzelm@9928

48 
Munich (Germany) http://isabelle.in.tum.de/dist/

nipkow@14023

49 

nipkow@14023

50 
Gerwin Klein

nipkow@14023

51 
Tobias Nipkow

nipkow@14023

52 
Larry Paulson
