changeset 9525 | 46fb9ccae463 |
parent 9487 | 7e377f912629 |
child 9713 | 2c5b42311eb0 |
9524:5721615da108 | 9525:46fb9ccae463 |
---|---|
45 next |
45 next |
46 assume "A --> B" and A |
46 assume "A --> B" and A |
47 thus B .. |
47 thus B .. |
48 qed |
48 qed |
49 |
49 |
50 lemmas atomize = all_eq imp_eq |
|
51 |
|
50 use "blastdata.ML" |
52 use "blastdata.ML" |
51 setup Blast.setup |
53 setup Blast.setup |
52 use "FOL_lemmas2.ML" |
54 use "FOL_lemmas2.ML" |
53 |
55 |
54 use "simpdata.ML" |
56 use "simpdata.ML" |