# HG changeset patch
# User haftmann
# Date 1231485764 -3600
# Node ID a462459fb5cea9c21600c63fd655dc8772a633a1
# Parent  89813bbf0f3e8bdd14826fade4c36137180e37a0# Parent  ebcd69a00872df7df555696525c41ec0ccd56f57
merged

diff -r ebcd69a00872 -r a462459fb5ce CONTRIBUTORS
--- a/CONTRIBUTORS	Thu Jan 08 17:10:41 2009 +0100
+++ b/CONTRIBUTORS	Fri Jan 09 08:22:44 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
diff -r ebcd69a00872 -r a462459fb5ce NEWS
--- a/NEWS	Thu Jan 08 17:10:41 2009 +0100
+++ b/NEWS	Fri Jan 09 08:22:44 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.