equal
deleted
inserted
replaced
50 subsection {* Lucas Dixon's eqstep tactic *} |
50 subsection {* Lucas Dixon's eqstep tactic *} |
51 |
51 |
52 use "~~/src/Provers/eqsubst.ML"; |
52 use "~~/src/Provers/eqsubst.ML"; |
53 use "eqrule_FOL_data.ML"; |
53 use "eqrule_FOL_data.ML"; |
54 |
54 |
55 setup EQSubstTac.setup |
55 setup EqSubst.setup |
56 |
56 |
57 |
57 |
58 subsection {* Other simple lemmas *} |
58 subsection {* Other simple lemmas *} |
59 |
59 |
60 lemma [simp]: "((P-->R) <-> (Q-->R)) <-> ((P<->Q) | R)" |
60 lemma [simp]: "((P-->R) <-> (Q-->R)) <-> ((P<->Q) | R)" |