1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/Errata.txt	Tue Nov 09 16:47:38 1993 +0100
     1.3 @@ -0,0 +1,27 @@
     1.4 +ERRATA FOR ISABELLE MANUAL
     1.5 +
     1.6 +** THM : BASIC INFERENCE **
     1.7 +
     1.8 +Pure/tactic/lift_inst_rule: now checks for distinct parameters (could also
     1.9 +compare with free variable names, though).  Variables in the insts are now
    1.10 +lifted over all parameters; their index is also increased.  Type vars in
    1.11 +the lhs variables are also increased by maxidx+1; this is essential for HOL
    1.12 +examples to work.
    1.13 +
    1.14 +
    1.15 +** THEORY MATTERS (GENERAL) **
    1.16 +
    1.17 +Definitions: users must ensure that the left-hand side is nothing
    1.18 +more complex than a function application -- never using fancy syntax.  E.g.
    1.19 +never
    1.20 +>     ("the_def",      "THE y. P(y) == Union({y . x:{0}, P(y)})" ),
    1.21 +but
    1.22 +<     ("the_def",      "The(P) == Union({y . x:{0}, P(y)})" ),
    1.23 +
    1.24 +Provers/classical, simp (new simplifier), tsimp (old simplifier), ind
    1.25 +
    1.26 +** SYSTEMS MATTERS **
    1.27 +
    1.28 +explain make system?  maketest
    1.29 +
    1.30 +expandshort