NEWS
changeset 68200 5859c688102a
parent 68157 057d5b4ce47e
child 68219 c0341c0080e2
     1.1 --- a/NEWS	Wed May 16 23:13:33 2018 +0200
     1.2 +++ b/NEWS	Thu May 17 07:42:33 2018 +0200
     1.3 @@ -262,6 +262,11 @@
     1.4  parametricity. See ~~/src/HOL/ex/Conditional_Parametricity_Examples for
     1.5  some examples.
     1.6  
     1.7 +* A new preprocessor for the code generator to generate code for algebraic
     1.8 +  types with lazy evaluation semantics even in call-by-value target languages.
     1.9 +  See theory HOL-Library.Code_Lazy for the implementation and
    1.10 +  HOL-Codegenerator_Test.Code_Lazy_Test for examples.
    1.11 +
    1.12  * SMT module:
    1.13    - The 'smt_oracle' option is now necessary when using the 'smt' method
    1.14      with a solver other than Z3. INCOMPATIBILITY.