1 Subject: Announcing Isabelle2012 
1 Subject: Announcing Isabelle2012 
2 To: isabelleusers@cl.cam.ac.uk 
2 To: isabelleusers@cl.cam.ac.uk 
3 
3 
4 Isabelle2012 is now available. 
4 Isabelle2012 is now available. 
5 
5 
6 This version significantly improves upon Isabelle20111, see the NEWS 
6 This version introduces many changes and improvements over 
7 file in the distribution for more details. Some notable changes are: 
7 Isabelle20111, see the NEWS file in the distribution for more 

8 details. Some highlights are: 
8 
9 
9 * FIXME 
10 * Improved Isabelle/jEdit Prover IDE (PIDE). 

11 

12 * Support for blockstructured specification contexts. 

13 

14 * Discontinued old code generator. 

15 

16 * Updated manuals: progprove, isarref, implementation, system. 

17 

18 * HOL: type 'a set is proper type constructor again. 

19 

20 * HOL: improved representation of numerals. 

21 

22 * HOL: new transfer and lifting packages, improved quotient package. 

23 

24 * HOL tool enhancements: Quickcheck, Nitpick, Sledgehammer. 

25 

26 * HOL library enhancements, including HOLLibrary and HOLProbability. 

27 

28 * HOL: more TPTP support. 

29 

30 * Reimplementation of HOLImport for HOLLight. 

31 

32 * ZF: some modernization of notation and proofs. 

33 

34 * System integration: improved support of Windows platform. 
10 
35 
11 
36 
12 You may get Isabelle2012 from the following mirror sites: 
37 You may get Isabelle2012 from the following mirror sites: 
13 
38 
14 Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ 
39 Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ 