NEWS
changeset 39644 ad436fa9fc5b
parent 39616 8052101883c3
child 39689 78b185bf7660
     1.1 --- a/NEWS	Thu Sep 23 08:30:33 2010 +0200
     1.2 +++ b/NEWS	Thu Sep 23 09:53:52 2010 +0200
     1.3 @@ -74,12 +74,16 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Improved infrastructure for term evaluation using code generator
     1.8 +techniques, in particular static evaluation conversions.
     1.9 +
    1.10  * String.literal is a type, but not a datatype. INCOMPATIBILITY.
    1.11   
    1.12  * Renamed lemmas:
    1.13    expand_fun_eq -> fun_eq_iff
    1.14    expand_set_eq -> set_eq_iff
    1.15    set_ext -> set_eqI
    1.16 + INCOMPATIBILITY.
    1.17  
    1.18  * Renamed class eq and constant eq (for code generation) to class equal
    1.19  and constant equal, plus renaming of related facts and various tuning.