doc-src/ERRATA.txt
changeset 716 79adbdbda0fb
parent 701 74ee8b9ff9a7
child 718 efca1e0710fb
--- a/doc-src/ERRATA.txt	Fri Nov 18 13:08:10 1994 +0100
+++ b/doc-src/ERRATA.txt	Fri Nov 18 13:14:23 1994 +0100
@@ -45,6 +45,10 @@
 
 page 145, line -5: delete repeated "the" in "before the the .thy file"
 
+Simplification
+
+page 158, "!": Isabelle now permits more general left-hand sides, so called
+higher-order patterns.
 
 ISABELLE'S OBJECT-LOGICS