clarifed
authorhaftmann
Fri Apr 20 15:13:06 2007 +0200 (2007-04-20)
changeset 227549947ae4792a0
parent 22753 49d7818e6161
child 22755 e268f608669a
clarifed
NEWS
     1.1 --- a/NEWS	Fri Apr 20 14:30:35 2007 +0200
     1.2 +++ b/NEWS	Fri Apr 20 15:13:06 2007 +0200
     1.3 @@ -66,7 +66,7 @@
     1.4  * code generator: 
     1.5    - Isar "definition"s and primitive instance definitions are added explicitly
     1.6      to the table of defining equations
     1.7 -  - primitive definitions are not unfolded by default any longer
     1.8 +  - primitive definitions are not used as defining equations by default any longer
     1.9    - defining equations are now definitly restricted to meta "==" and object
    1.10          equality "="
    1.11    - HOL theories have been adopted accordingly