--- a/CONTRIBUTORS Thu Jan 08 10:53:48 2009 +0100
+++ b/CONTRIBUTORS Thu Jan 08 17:25:06 2009 +0100
@@ -7,12 +7,19 @@
Contributions to this Isabelle version
--------------------------------------
+* December 2008: Clemens Ballarin, TUM
+ New locale implementation.
+
* December 2008: Armin Heller, TUM and Alexander Krauss, TUM
Method "sizechange" for advanced termination proofs.
* November 2008: Timothy Bourke, NICTA
Performance improvement (factor 50) for find_theorems.
+* 2008: Florian Haftmann, TUM
+ Various extensions and restructurings in HOL, improvements
+ in evaluation mechanisms, new module binding.ML for name bindings.
+
* October 2008: Fabian Immler, TUM
ATP manager for Sledgehammer, based on ML threads instead of Posix
processes. Additional ATP wrappers, including remote SystemOnTPTP
--- a/NEWS Thu Jan 08 10:53:48 2009 +0100
+++ b/NEWS Thu Jan 08 17:25:06 2009 +0100
@@ -236,6 +236,13 @@
src/HOL/Real/rat_arith.ML ~> src/HOL/Tools
src/HOL/Real/real_arith.ML ~> src/HOL/Tools
+ src/HOL/Library/Array.thy ~> src/HOL/Imperative_HOL
+ src/HOL/Library/Heap_Monad.thy ~> src/HOL/Imperative_HOL
+ src/HOL/Library/Heap.thy ~> src/HOL/Imperative_HOL
+ src/HOL/Library/Imperative_HOL.thy ~> src/HOL/Imperative_HOL
+ src/HOL/Library/Ref.thy ~> src/HOL/Imperative_HOL
+ src/HOL/Library/Relational.thy ~> src/HOL/Imperative_HOL
+
* If methods "eval" and "evaluation" encounter a structured proof state
with !!/==>, only the conclusion is evaluated to True (if possible),
avoiding strange error messages.