5 
5 
6 This release improves upon Isabelle2009 in many ways, see the NEWS 
6 This release improves upon Isabelle2009 in many ways, see the NEWS 
7 file in the distribution for more details. Some important changes 
7 file in the distribution for more details. Some important changes 
8 are: 
8 are: 
9 
9 
10 * Proof method "smt" for a combination of firstorder logic with equality, 
10 * Isabelle tool "wwwfind" provides web interface for 'find_theorems' 
11 linear and nonlinear (natural/integer/real) arithmetic, and fixedsize bitvectors. 
11 on a given logic image. 
12 
12 
13 * Counterexample generator tool »nitpick« based on the Kodkod relational model finder. 
13 * HOLSMT: proof method "smt" for a combination of firstorder logic 
14 
14 with equality, linear and nonlinear (natural/integer/real) arithmetic, 
15 * Predicate compiler turning inductive into (executable) equational specifications. 
15 and fixedsize bitvectors. 
16 

17 * Refined number theory. 

18 

19 * Various parts of multivariate analysis. 

20 
16 
21 * HOLBoogie: an interactive prover backend for Boogie and VCC. 
17 * HOLBoogie: an interactive prover backend for Boogie and VCC. 
22 
18 

19 * HOL: Counterexample generator tool Nitpick based on the Kodkod 

20 relational model finder. 

21 

22 * HOL: predicate compiler turning inductive into (executable) 

23 equational specifications. 

24 

25 * HOL: refined number theory. 

26 

27 * HOL: various parts of multivariate analysis. 

28 

29 * HOLCF: new definitional domain package. 

30 
23 * Revised tutorial on locales. 
31 * Revised tutorial on locales. 
24 
32 
25 * New definitional domain package for HOLCF. 
33 * Support for Poly/ML 5.3.0, with improved reporting of compiler 

34 errors and runtime exceptions, including detailed source positions. 
26 
35 
27 * Support for Poly/ML 5.3.0, with improved reporting of compiler errors and runtime exceptions, including detailed source positions. 
36 * Parallel checking of nested Isar proofs, with improved scalability 

37 up to 8 cores. 

38 
28 
39 
29 You may get Isabelle20091 from the following mirror sites: 
40 You may get Isabelle20091 from the following mirror sites: 
30 
41 
31 Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ 
42 Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ 
32 Munich (Germany) http://isabelle.in.tum.de/ 
43 Munich (Germany) http://isabelle.in.tum.de/ 