--- a/CONTRIBUTORS Wed May 16 23:13:33 2018 +0200
+++ b/CONTRIBUTORS Thu May 17 07:42:33 2018 +0200
@@ -14,6 +14,10 @@
* May 2018: Florian Haftmann
Consolidation of string-like types in HOL.
+* May 2018: Andreas Lochbihler (Digital Asset),
+ Pascal Stoop (ETH Zurich)
+ Code generation with lazy evaluation semantics.
+
* March 2018: Florian Haftmann
Abstract bit operations push_bit, take_bit, drop_bit, alongside
with an algebraic foundation for bit strings and word types in
--- 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.