# 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 (-) + writing ML code to a file: + code_serialize ml () + writing Haskell code to a bunch of files: + code_serialize haskell () + +See HOL/ex/Codegenerator.thy for examples. + * Command 'no_translations' removes translation rules from theory syntax.