NEWS
changeset 29398 89813bbf0f3e
parent 29253 3c6cd80a4854
child 29608 564ea783ace8
     1.1 --- a/NEWS	Thu Jan 08 10:53:48 2009 +0100
     1.2 +++ b/NEWS	Thu Jan 08 17:25:06 2009 +0100
     1.3 @@ -236,6 +236,13 @@
     1.4      src/HOL/Real/rat_arith.ML ~> src/HOL/Tools
     1.5      src/HOL/Real/real_arith.ML ~> src/HOL/Tools
     1.6  
     1.7 +    src/HOL/Library/Array.thy ~> src/HOL/Imperative_HOL
     1.8 +    src/HOL/Library/Heap_Monad.thy ~> src/HOL/Imperative_HOL
     1.9 +    src/HOL/Library/Heap.thy ~> src/HOL/Imperative_HOL
    1.10 +    src/HOL/Library/Imperative_HOL.thy ~> src/HOL/Imperative_HOL
    1.11 +    src/HOL/Library/Ref.thy ~> src/HOL/Imperative_HOL
    1.12 +    src/HOL/Library/Relational.thy ~> src/HOL/Imperative_HOL
    1.13 +
    1.14  * If methods "eval" and "evaluation" encounter a structured proof state
    1.15  with !!/==>, only the conclusion is evaluated to True (if possible),
    1.16  avoiding strange error messages.