equal
deleted
inserted
replaced
250 |
250 |
251 subsubsection {* Classical Reasoner setup *} |
251 subsubsection {* Classical Reasoner setup *} |
252 |
252 |
253 use "cladata.ML" |
253 use "cladata.ML" |
254 setup hypsubst_setup |
254 setup hypsubst_setup |
|
255 |
255 declare atomize_all [symmetric, rulify] atomize_imp [symmetric, rulify] |
256 declare atomize_all [symmetric, rulify] atomize_imp [symmetric, rulify] |
|
257 |
256 setup Classical.setup |
258 setup Classical.setup |
257 setup clasetup |
259 setup clasetup |
|
260 |
|
261 declare ext [intro?] |
|
262 declare disjI1 [elim?] disjI2 [elim?] ex1_implies_ex [elim?] sym [elim?] |
258 |
263 |
259 use "blastdata.ML" |
264 use "blastdata.ML" |
260 setup Blast.setup |
265 setup Blast.setup |
261 |
266 |
262 |
267 |