--- a/NEWS Wed May 16 23:13:33 2018 +0200
+++ b/NEWS Thu May 17 07:42:33 2018 +0200
@@ -262,6 +262,11 @@
parametricity. See ~~/src/HOL/ex/Conditional_Parametricity_Examples for
some examples.
+* A new preprocessor for the code generator to generate code for algebraic
+ types with lazy evaluation semantics even in call-by-value target languages.
+ See theory HOL-Library.Code_Lazy for the implementation and
+ HOL-Codegenerator_Test.Code_Lazy_Test for examples.
+
* SMT module:
- The 'smt_oracle' option is now necessary when using the 'smt' method
with a solver other than Z3. INCOMPATIBILITY.