Updates involving defs, addss, etc.
authorlcp
Wed May 03 11:58:40 1995 +0200 (1995-05-03)
changeset 108353a0667e1cd2
parent 1082 1b30e27aca82
child 1084 502a61cbf37b
Updates involving defs, addss, etc.
doc-src/ERRATA.txt
     1.1 --- a/doc-src/ERRATA.txt	Wed May 03 08:58:32 1995 +0200
     1.2 +++ b/doc-src/ERRATA.txt	Wed May 03 11:58:40 1995 +0200
     1.3 @@ -12,6 +12,10 @@
     1.4  
     1.5  Advanced Methods
     1.6  
     1.7 +page 46: the theory sections can appear in any order
     1.8 +
     1.9 +page 48: theories may now contain a separate definition part
    1.10 +
    1.11  page 52, middle: the declaration "types bool,nat" should be "types bool nat"
    1.12  
    1.13  page 57, bottom: should be addsimps in 
    1.14 @@ -56,8 +60,9 @@
    1.15  
    1.16  Classical reasoner
    1.17  
    1.18 -page 176: The package also provides tactics slow_tac, slow_best_tac, depth_tac
    1.19 -and deepen_tac. 
    1.20 +page 176: Classical sets may specify a "wrapper tactical", which can be used
    1.21 +to define addss.  The package also provides tactics slow_tac, slow_best_tac,
    1.22 +depth_tac and deepen_tac.
    1.23  
    1.24  ISABELLE'S OBJECT-LOGICS
    1.25