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