# HG changeset patch
# User haftmann
# Date 1153838611 -7200
# Node ID 8b22026445af435b1efa0c2035613bd9c035dec9
# Parent  af47971ea30493a09765b275f45d6eacbcb30bd5
added notes on class_package.ML and codegen_package.ML

diff -r af47971ea304 -r 8b22026445af NEWS
--- a/NEWS	Sun Jul 23 07:21:41 2006 +0200
+++ b/NEWS	Tue Jul 25 16:43:31 2006 +0200
@@ -37,6 +37,21 @@
 
 *** Pure ***
 
+* 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.
+
+* Yet another code generator framework allows to generate executable code
+for ML and Haskell (including "class"es). Most basic use cases:
+
+    internal compilation:
+        code_serialize ml <list of constants (term syntax)> (-)
+    writing ML code to a file:
+        code_serialize ml <list of constants (term syntax)> (<filename>)
+    writing Haskell code to a bunch of files:
+        code_serialize haskell <list of constants (term syntax)> (<filename>)
+
+See HOL/ex/Codegenerator.thy for examples.
+
 * Command 'no_translations' removes translation rules from theory
 syntax.