| changeset 12303 | 67ca723a02dd |
| parent 12240 | 0760eda193c4 |
| child 12367 | 1cee8a0db392 |
| 12302:87d1bddcdfe7 | 12303:67ca723a02dd |
|---|---|
23 theorems case_split = case_split_thm [case_names True False, cases type: o] |
23 theorems case_split = case_split_thm [case_names True False, cases type: o] |
24 |
24 |
25 use "cladata.ML" |
25 use "cladata.ML" |
26 setup Cla.setup |
26 setup Cla.setup |
27 setup clasetup |
27 setup clasetup |
28 |
|
29 declare disjI1 [elim?] disjI2 [elim?] |
|
28 |
30 |
29 use "blastdata.ML" |
31 use "blastdata.ML" |
30 setup Blast.setup |
32 setup Blast.setup |
31 use "FOL_lemmas2.ML" |
33 use "FOL_lemmas2.ML" |
32 |
34 |