author | wenzelm |

Sat May 05 18:21:55 2012 +0200 (2012-05-05) | |

changeset 47869 | fa59eb662e6c |

parent 47868 | 32c03d45fffe |

child 47870 | ec815d64573f |

some highlights of Isabelle2012;

1.1 --- a/ANNOUNCE Fri May 04 17:14:42 2012 +0200 1.2 +++ b/ANNOUNCE Sat May 05 18:21:55 2012 +0200 1.3 @@ -3,10 +3,35 @@ 1.4 1.5 Isabelle2012 is now available. 1.6 1.7 -This version significantly improves upon Isabelle2011-1, see the NEWS 1.8 -file in the distribution for more details. Some notable changes are: 1.9 +This version introduces many changes and improvements over 1.10 +Isabelle2011-1, see the NEWS file in the distribution for more 1.11 +details. Some highlights are: 1.12 + 1.13 +* Improved Isabelle/jEdit Prover IDE (PIDE). 1.14 + 1.15 +* Support for block-structured specification contexts. 1.16 + 1.17 +* Discontinued old code generator. 1.18 + 1.19 +* Updated manuals: prog-prove, isar-ref, implementation, system. 1.20 + 1.21 +* HOL: type 'a set is proper type constructor again. 1.22 1.23 -* FIXME 1.24 +* HOL: improved representation of numerals. 1.25 + 1.26 +* HOL: new transfer and lifting packages, improved quotient package. 1.27 + 1.28 +* HOL tool enhancements: Quickcheck, Nitpick, Sledgehammer. 1.29 + 1.30 +* HOL library enhancements, including HOL-Library and HOL-Probability. 1.31 + 1.32 +* HOL: more TPTP support. 1.33 + 1.34 +* Re-implementation of HOL-Import for HOL-Light. 1.35 + 1.36 +* ZF: some modernization of notation and proofs. 1.37 + 1.38 +* System integration: improved support of Windows platform. 1.39 1.40 1.41 You may get Isabelle2012 from the following mirror sites: