NEWS
changeset 52435 6646bb548c6b
parent 52430 289e36c2870a
child 52439 4cf3f6153eb8
--- a/NEWS	Sun Jun 23 21:16:06 2013 +0200
+++ b/NEWS	Sun Jun 23 21:16:07 2013 +0200
@@ -68,6 +68,12 @@
 
 *** HOL ***
 
+* Code generator:
+  * 'code_printing' unifies 'code_const' / 'code_type' / 'code_class' / 'code_instance'.
+  * 'code_identifier' declares name hints for arbitrary identifiers in generated code,
+    subsuming 'code_modulename'.
+  See the Isar reference manual for syntax diagrams, and the HOL theories for examples.
+
 * Library/Polynomial.thy:
   * Use lifting for primitive definitions.
   * Explicit conversions from and to lists of coefficients, used for generated code.