NEWS
changeset 38524 c3f2e9986e30
parent 38522 de7984a7172b
child 38546 5c69afe3df06
     1.1 --- a/NEWS	Wed Aug 18 12:27:39 2010 +0200
     1.2 +++ b/NEWS	Wed Aug 18 14:55:09 2010 +0200
     1.3 @@ -77,6 +77,8 @@
     1.4      nat ~> Nat.nat
     1.5  
     1.6    constants
     1.7 +    Let ~> HOL.Let
     1.8 +    If ~> HOL.If
     1.9      Ball ~> Set.Ball
    1.10      Bex ~> Set.Bex
    1.11      Suc ~> Nat.Suc
    1.12 @@ -90,7 +92,7 @@
    1.13  INCOMPATIBILITY.
    1.14  
    1.15  * Removed simplifier congruence rule of "prod_case", as has for long
    1.16 -been the case with "split".
    1.17 +been the case with "split".  INCOMPATIBILITY.
    1.18  
    1.19  * Datatype package: theorems generated for executable equality
    1.20  (class eq) carry proper names and are treated as default code
    1.21 @@ -99,8 +101,8 @@
    1.22  * List.thy: use various operations from the Haskell prelude when
    1.23  generating Haskell code.
    1.24  
    1.25 -* code_simp.ML: simplification with rules determined by
    1.26 -code generator.
    1.27 +* code_simp.ML and method code_simp: simplification with rules determined
    1.28 +by code generator.
    1.29  
    1.30  * code generator: do not print function definitions for case
    1.31  combinators any longer.