# HG changeset patch
# User wenzelm
# Date 1358687137 -3600
# Node ID c633700b2d9fe8879e735f68d1c3e8a7fc5532ab
# Parent  5231bfb8bfcf96484a928ebefaf98df28b489073# Parent  b3c6c9ef11b804b99c648ca42e3ed3fefeba3056
merged

diff -r 5231bfb8bfcf -r c633700b2d9f ANNOUNCE
--- a/ANNOUNCE	Sat Jan 19 22:18:35 2013 +0100
+++ b/ANNOUNCE	Sun Jan 20 14:05:37 2013 +0100
@@ -1,40 +1,16 @@
-Subject: Announcing Isabelle2012
+Subject: Announcing Isabelle2013
 To: isabelle-users@cl.cam.ac.uk
 
-Isabelle2012 is now available.
-
-This version introduces many changes and improvements over
-Isabelle2011-1, see the NEWS file in the distribution for more
-details.  Some highlights are:
-
-* Improved Isabelle/jEdit Prover IDE (PIDE).
-
-* Support for block-structured specification contexts.
-
-* Discontinued old code generator.
-
-* Updated manuals: prog-prove, isar-ref, implementation, system.
-
-* HOL: type 'a set is proper type constructor again.
+Isabelle2013 is now available.
 
-* HOL: improved representation of numerals.
-
-* HOL: new transfer and lifting packages, improved quotient package.
-
-* HOL tool enhancements: Quickcheck, Nitpick, Sledgehammer.
-
-* HOL library enhancements, including HOL-Library and HOL-Probability.
+This version consolidates Isabelle2012 and introduces numerous
+improvements, see the NEWS file in the distribution for more details.
+Some highlights are:
 
-* HOL: more TPTP support.
-
-* Re-implementation of HOL-Import for HOL-Light.
-
-* ZF: some modernization of notation and proofs.
-
-* System integration: improved support of Windows platform.
+* FIXME
 
 
-You may get Isabelle2012 from the following mirror sites:
+You may get Isabelle2013 from the following mirror sites:
 
   Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
   Munich (Germany)     http://isabelle.in.tum.de/
diff -r 5231bfb8bfcf -r c633700b2d9f Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST	Sat Jan 19 22:18:35 2013 +0100
+++ b/Admin/Release/CHECKLIST	Sun Jan 20 14:05:37 2013 +0100
@@ -15,8 +15,6 @@
 
 - check HTML header of library;
 
-- check persistent sessions with PG and Poly/ML 5.x;
-
 - check file positions within logic images (hyperlinks etc.);
 
 - isabelle update_keywords;
@@ -44,7 +42,6 @@
 
 - test contrib components:
     x86_64-linux without 32bit C/C++ libraries
-    Mac OS X Leopard
 
 - check "Handler catches all exceptions", using
   PolyML.Compiler.reportExhaustiveHandlers := true;
diff -r 5231bfb8bfcf -r c633700b2d9f CONTRIBUTORS
--- a/CONTRIBUTORS	Sat Jan 19 22:18:35 2013 +0100
+++ b/CONTRIBUTORS	Sun Jan 20 14:05:37 2013 +0100
@@ -18,7 +18,7 @@
   including a smart type annotation algorithm and proof shrinking.
 
 * December 2012: Alessandro Coglio, Kestrel
-  Contributions to HOL's Lattice library
+  Contributions to HOL's Lattice library.
 
 * November 2012: Fabian Immler, TUM
   "Symbols" dockable for Isabelle/jEdit.
diff -r 5231bfb8bfcf -r c633700b2d9f NEWS
--- a/NEWS	Sat Jan 19 22:18:35 2013 +0100
+++ b/NEWS	Sun Jan 20 14:05:37 2013 +0100
@@ -379,7 +379,7 @@
 with support for mixed, nested recursion and interesting non-free
 datatypes.
 
-* HOL/Finite_Set and Relation: added new set and relation operations 
+* HOL/Finite_Set and Relation: added new set and relation operations
 expressed by Finite_Set.fold.
 
 * New theory HOL/Library/RBT_Set: implementation of sets by red-black
diff -r 5231bfb8bfcf -r c633700b2d9f src/Pure/Tools/task_statistics.scala
--- a/src/Pure/Tools/task_statistics.scala	Sat Jan 19 22:18:35 2013 +0100
+++ b/src/Pure/Tools/task_statistics.scala	Sun Jan 20 14:05:37 2013 +0100
@@ -33,7 +33,7 @@
   {
     val values = new Array[Double](tasks.length)
     for ((Run(x), i) <- tasks.iterator.zipWithIndex) values(i) =
-      Math.log10(x.toDouble / 1000000)
+      java.lang.Math.log10(x.toDouble / 1000000)
 
     val data = new HistogramDataset
     data.addSeries("tasks", values, bins)