# HG changeset patch
# User lcp
# Date 799495120 -7200
# Node ID 53a0667e1cd228b27c313803174b76188bdc9a01
# Parent  1b30e27aca826552e9d77c580765edb62e3a8348
Updates involving defs, addss, etc.

diff -r 1b30e27aca82 -r 53a0667e1cd2 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