Updates involving defs, addss, etc.
--- a/doc-src/ERRATA.txt Wed May 03 08:58:32 1995 +0200
+++ b/doc-src/ERRATA.txt Wed May 03 11:58:40 1995 +0200
@@ -12,6 +12,10 @@
Advanced Methods
+page 46: the theory sections can appear in any order
+
+page 48: theories may now contain a separate definition part
+
page 52, middle: the declaration "types bool,nat" should be "types bool nat"
page 57, bottom: should be addsimps in
@@ -56,8 +60,9 @@
Classical reasoner
-page 176: The package also provides tactics slow_tac, slow_best_tac, depth_tac
-and deepen_tac.
+page 176: Classical sets may specify a "wrapper tactical", which can be used
+to define addss. The package also provides tactics slow_tac, slow_best_tac,
+depth_tac and deepen_tac.
ISABELLE'S OBJECT-LOGICS