# HG changeset patch
# User haftmann
# Date 1177060893 -7200
# Node ID cf627add250ae142b5649a947f40a4fa61aec3ce
# Parent  790f73fa8b369c0efea33f57985914bda87d4d88
code generator changes

diff -r 790f73fa8b36 -r cf627add250a NEWS
--- a/NEWS	Fri Apr 20 10:09:32 2007 +0200
+++ b/NEWS	Fri Apr 20 11:21:33 2007 +0200
@@ -63,6 +63,14 @@
 
 *** Pure ***
 
+* 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
+  - defining equations are now definitly restricted to meta "==" and object
+        equality "="
+  - HOL theories have been adopted accordingly
+
 * class_package.ML offers a combination of axclasses and locales to
 achieve Haskell-like type classes in Isabelle. See
 HOL/ex/Classpackage.thy for examples.
@@ -74,6 +82,8 @@
         code_gen <list of constants (term syntax)> (SML #)
     writing SML code to a file:
         code_gen <list of constants (term syntax)> (SML <filename>)
+    writing OCaml code to a file:
+        code_gen <list of constants (term syntax)> (OCaml <filename>)
     writing Haskell code to a bunch of files:
         code_gen <list of constants (term syntax)> (Haskell <filename>)
 
@@ -86,7 +96,7 @@
     [code inline]:    select an equation theorem for unfolding (inlining) in place
     [code noinline]:  deselect an equation theorem for unfolding (inlining) in place
 
-User-defined serializations (target in {SML, Haskell}):
+User-defined serializations (target in {SML, OCaml, Haskell}):
 
     code_const <and-list of constants (term syntax)>
       {(target) <and-list of const target syntax>}+
@@ -102,10 +112,10 @@
       {(target) <and-list of class target syntax>}+
         where class target syntax ::= <class name> {where {<classop> == <target syntax>}+}?
 
-For code_instance and code_class, target SML is silently ignored.
-
-See HOL theories and HOL/ex/Code*.thy for usage examples.  Doc/Isar/Advanced/Codegen/
-provides a tutorial.
+code_instance and code_class only apply to target Haskell.
+
+See HOL theories and HOL/ex/Codegenerator*.thy for usage examples.
+Doc/Isar/Advanced/Codegen/ provides a tutorial.
 
 * Command 'no_translations' removes translation rules from theory
 syntax.
@@ -505,6 +515,9 @@
 
 *** HOL ***
 
+* Library/Commutative_Ring.thy: switched from recdef to function package;
+    constants add, mul, pow now curried.  Infix syntax for algebraic operations.
+
 * Some steps towards more uniform lattice theory development in HOL.
 
     constants "meet" and "join" now named "inf" and "sup"