Updates involving defs, addss, etc.
authorlcp
Wed, 03 May 1995 11:58:40 +0200
changeset 1083 53a0667e1cd2
parent 1082 1b30e27aca82
child 1084 502a61cbf37b
Updates involving defs, addss, etc.
doc-src/ERRATA.txt
--- 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