NEWS
changeset 22921 475ff421a6a3
parent 22871 9ffb43b19ec6
child 22965 b81bbe298406
     1.1 --- a/NEWS	Thu May 10 10:21:50 2007 +0200
     1.2 +++ b/NEWS	Thu May 10 10:22:17 2007 +0200
     1.3 @@ -68,20 +68,23 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* code generator: consts in 'consts_code' Isar commands are now referred
     1.8 +  to by usual term syntax (including optional type annotations).
     1.9 +
    1.10  * code generator: 
    1.11 -  - Isar "definition"s and primitive instance definitions are added explicitly
    1.12 -    to the table of defining equations
    1.13 +  - Isar 'definition's, 'constdef's and primitive instance definitions are added
    1.14 +    explicitly to the table of defining equations
    1.15    - primitive definitions are not used as defining equations by default any longer
    1.16    - defining equations are now definitly restricted to meta "==" and object
    1.17          equality "="
    1.18    - HOL theories have been adopted accordingly
    1.19  
    1.20  * class_package.ML offers a combination of axclasses and locales to
    1.21 -achieve Haskell-like type classes in Isabelle. See
    1.22 +achieve Haskell-like type classes in Isabelle.  See
    1.23  HOL/ex/Classpackage.thy for examples.
    1.24  
    1.25  * Yet another code generator framework allows to generate executable
    1.26 -code for ML and Haskell (including "class"es). A short usage sketch:
    1.27 +code for ML and Haskell (including "class"es).  A short usage sketch:
    1.28  
    1.29      internal compilation:
    1.30          code_gen <list of constants (term syntax)> (SML #)