1.1 --- a/ANNOUNCE Sat Jan 19 22:18:35 2013 +0100
1.2 +++ b/ANNOUNCE Sun Jan 20 14:05:37 2013 +0100
1.3 @@ -1,40 +1,16 @@
1.4 -Subject: Announcing Isabelle2012
1.5 +Subject: Announcing Isabelle2013
1.6 To: isabelle-users@cl.cam.ac.uk
1.7
1.8 -Isabelle2012 is now available.
1.9 +Isabelle2013 is now available.
1.10
1.11 -This version introduces many changes and improvements over
1.12 -Isabelle2011-1, see the NEWS file in the distribution for more
1.13 -details. Some highlights are:
1.14 +This version consolidates Isabelle2012 and introduces numerous
1.15 +improvements, see the NEWS file in the distribution for more details.
1.16 +Some highlights are:
1.17
1.18 -* Improved Isabelle/jEdit Prover IDE (PIDE).
1.19 +* FIXME
1.20
1.21 -* Support for block-structured specification contexts.
1.22
1.23 -* Discontinued old code generator.
1.24 -
1.25 -* Updated manuals: prog-prove, isar-ref, implementation, system.
1.26 -
1.27 -* HOL: type 'a set is proper type constructor again.
1.28 -
1.29 -* HOL: improved representation of numerals.
1.30 -
1.31 -* HOL: new transfer and lifting packages, improved quotient package.
1.32 -
1.33 -* HOL tool enhancements: Quickcheck, Nitpick, Sledgehammer.
1.34 -
1.35 -* HOL library enhancements, including HOL-Library and HOL-Probability.
1.36 -
1.37 -* HOL: more TPTP support.
1.38 -
1.39 -* Re-implementation of HOL-Import for HOL-Light.
1.40 -
1.41 -* ZF: some modernization of notation and proofs.
1.42 -
1.43 -* System integration: improved support of Windows platform.
1.44 -
1.45 -
1.46 -You may get Isabelle2012 from the following mirror sites:
1.47 +You may get Isabelle2013 from the following mirror sites:
1.48
1.49 Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/
1.50 Munich (Germany) http://isabelle.in.tum.de/
2.1 --- a/Admin/Release/CHECKLIST Sat Jan 19 22:18:35 2013 +0100
2.2 +++ b/Admin/Release/CHECKLIST Sun Jan 20 14:05:37 2013 +0100
2.3 @@ -15,8 +15,6 @@
2.4
2.5 - check HTML header of library;
2.6
2.7 -- check persistent sessions with PG and Poly/ML 5.x;
2.8 -
2.9 - check file positions within logic images (hyperlinks etc.);
2.10
2.11 - isabelle update_keywords;
2.12 @@ -44,7 +42,6 @@
2.13
2.14 - test contrib components:
2.15 x86_64-linux without 32bit C/C++ libraries
2.16 - Mac OS X Leopard
2.17
2.18 - check "Handler catches all exceptions", using
2.19 PolyML.Compiler.reportExhaustiveHandlers := true;
3.1 --- a/CONTRIBUTORS Sat Jan 19 22:18:35 2013 +0100
3.2 +++ b/CONTRIBUTORS Sun Jan 20 14:05:37 2013 +0100
3.3 @@ -18,7 +18,7 @@
3.4 including a smart type annotation algorithm and proof shrinking.
3.5
3.6 * December 2012: Alessandro Coglio, Kestrel
3.7 - Contributions to HOL's Lattice library
3.8 + Contributions to HOL's Lattice library.
3.9
3.10 * November 2012: Fabian Immler, TUM
3.11 "Symbols" dockable for Isabelle/jEdit.
4.1 --- a/NEWS Sat Jan 19 22:18:35 2013 +0100
4.2 +++ b/NEWS Sun Jan 20 14:05:37 2013 +0100
4.3 @@ -379,7 +379,7 @@
4.4 with support for mixed, nested recursion and interesting non-free
4.5 datatypes.
4.6
4.7 -* HOL/Finite_Set and Relation: added new set and relation operations
4.8 +* HOL/Finite_Set and Relation: added new set and relation operations
4.9 expressed by Finite_Set.fold.
4.10
4.11 * New theory HOL/Library/RBT_Set: implementation of sets by red-black
5.1 --- a/src/Pure/Tools/task_statistics.scala Sat Jan 19 22:18:35 2013 +0100
5.2 +++ b/src/Pure/Tools/task_statistics.scala Sun Jan 20 14:05:37 2013 +0100
5.3 @@ -33,7 +33,7 @@
5.4 {
5.5 val values = new Array[Double](tasks.length)
5.6 for ((Run(x), i) <- tasks.iterator.zipWithIndex) values(i) =
5.7 - Math.log10(x.toDouble / 1000000)
5.8 + java.lang.Math.log10(x.toDouble / 1000000)
5.9
5.10 val data = new HistogramDataset
5.11 data.addSeries("tasks", values, bins)