equal
deleted
inserted
replaced
8 |
8 |
9 (*Higher precedence than := facilitates use of references*) |
9 (*Higher precedence than := facilitates use of references*) |
10 infix 4 add_safes add_unsafes; |
10 infix 4 add_safes add_unsafes; |
11 |
11 |
12 structure Cla = |
12 structure Cla = |
13 |
|
14 struct |
13 struct |
15 |
14 |
16 datatype pack = Pack of thm list * thm list; |
15 datatype pack = Pack of thm list * thm list; |
17 |
16 |
18 val trace = ref false; |
17 val trace = Unsynchronized.ref false; |
19 |
18 |
20 (*A theorem pack has the form (safe rules, unsafe rules) |
19 (*A theorem pack has the form (safe rules, unsafe rules) |
21 An unsafe rule is incomplete or introduces variables in subgoals, |
20 An unsafe rule is incomplete or introduces variables in subgoals, |
22 and is tried only when the safe rules are not applicable. *) |
21 and is tried only when the safe rules are not applicable. *) |
23 |
22 |