--- a/NEWS Sun Jul 15 18:22:31 2018 +0100
+++ b/NEWS Sun Jul 15 23:44:52 2018 +0200
@@ -379,8 +379,9 @@
* Theory HOL-Library.Code_Lazy provides 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-Codegenerator_Test.Code_Lazy_Test for some examples.
+semantics even in call-by-value target languages. See the theories
+HOL-ex.Code_Lazy_Demo and HOL-Codegenerator_Test.Code_Lazy_Test for
+some examples.
* Theory HOL-Library.Landau_Symbols has been moved here from AFP.