equal
deleted
inserted
replaced

1 ERRATA FOR ISABELLE MANUAL 

2 

3 ** THM : BASIC INFERENCE ** 

4 

5 Pure/tactic/lift_inst_rule: now checks for distinct parameters (could also 

6 compare with free variable names, though). Variables in the insts are now 

7 lifted over all parameters; their index is also increased. Type vars in 

8 the lhs variables are also increased by maxidx+1; this is essential for HOL 

9 examples to work. 

10 

11 

12 ** THEORY MATTERS (GENERAL) ** 

13 

14 Definitions: users must ensure that the lefthand side is nothing 

15 more complex than a function application  never using fancy syntax. E.g. 

16 never 

17 > ("the_def", "THE y. P(y) == Union({y . x:{0}, P(y)})" ), 

18 but 

19 < ("the_def", "The(P) == Union({y . x:{0}, P(y)})" ), 

20 

21 Provers/classical, simp (new simplifier), tsimp (old simplifier), ind 

22 

23 ** SYSTEMS MATTERS ** 

24 

25 explain make system? maketest 

26 

27 expandshort 