equal
deleted
inserted
replaced
117 |
117 |
118 subsection {* Lemmas and proof tools *} |
118 subsection {* Lemmas and proof tools *} |
119 |
119 |
120 setup Simplifier.setup |
120 setup Simplifier.setup |
121 use "IFOL_lemmas.ML" |
121 use "IFOL_lemmas.ML" |
|
122 |
|
123 declare impE [Pure.elim] iffD1 [Pure.elim] iffD2 [Pure.elim] |
|
124 |
122 use "fologic.ML" |
125 use "fologic.ML" |
123 use "hypsubstdata.ML" |
126 use "hypsubstdata.ML" |
124 setup hypsubst_setup |
127 setup hypsubst_setup |
125 use "intprover.ML" |
128 use "intprover.ML" |
126 |
129 |