1.1 --- a/CONTRIBUTORS	Thu Jan 08 10:53:48 2009 +0100
     1.2 +++ b/CONTRIBUTORS	Thu Jan 08 17:25:06 2009 +0100
     1.3 @@ -7,12 +7,19 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* December 2008: Clemens Ballarin, TUM
     1.8 +  New locale implementation.
     1.9 +
    1.10  * December 2008: Armin Heller, TUM and Alexander Krauss, TUM
    1.11    Method "sizechange" for advanced termination proofs.
    1.12  
    1.13  * November 2008: Timothy Bourke, NICTA
    1.14    Performance improvement (factor 50) for find_theorems.
    1.15  
    1.16 +* 2008: Florian Haftmann, TUM
    1.17 +  Various extensions and restructurings in HOL, improvements
    1.18 +  in evaluation mechanisms, new module binding.ML for name bindings.
    1.19 +
    1.20  * October 2008: Fabian Immler, TUM
    1.21    ATP manager for Sledgehammer, based on ML threads instead of Posix
    1.22    processes.  Additional ATP wrappers, including remote SystemOnTPTP

     2.1 --- a/NEWS	Thu Jan 08 10:53:48 2009 +0100
     2.2 +++ b/NEWS	Thu Jan 08 17:25:06 2009 +0100
     2.3 @@ -236,6 +236,13 @@
     2.4      src/HOL/Real/rat_arith.ML ~> src/HOL/Tools
     2.5      src/HOL/Real/real_arith.ML ~> src/HOL/Tools
     2.6  
     2.7 +    src/HOL/Library/Array.thy ~> src/HOL/Imperative_HOL
     2.8 +    src/HOL/Library/Heap_Monad.thy ~> src/HOL/Imperative_HOL
     2.9 +    src/HOL/Library/Heap.thy ~> src/HOL/Imperative_HOL
    2.10 +    src/HOL/Library/Imperative_HOL.thy ~> src/HOL/Imperative_HOL
    2.11 +    src/HOL/Library/Ref.thy ~> src/HOL/Imperative_HOL
    2.12 +    src/HOL/Library/Relational.thy ~> src/HOL/Imperative_HOL
    2.13 +
    2.14  * If methods "eval" and "evaluation" encounter a structured proof state
    2.15  with !!/==>, only the conclusion is evaluated to True (if possible),
    2.16  avoiding strange error messages.