equal
deleted
inserted
replaced
633 lemmas [Pure.elim!] = disjE iffE FalseE conjE exE |
633 lemmas [Pure.elim!] = disjE iffE FalseE conjE exE |
634 and [Pure.intro!] = iffI conjI impI TrueI notI allI refl |
634 and [Pure.intro!] = iffI conjI impI TrueI notI allI refl |
635 and [Pure.elim 2] = allE notE' impE' |
635 and [Pure.elim 2] = allE notE' impE' |
636 and [Pure.intro] = exI disjI2 disjI1 |
636 and [Pure.intro] = exI disjI2 disjI1 |
637 |
637 |
638 setup {* Context_Rules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac) *} |
638 setup {* Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac ctxt ORELSE' tac) *} |
639 |
639 |
640 |
640 |
641 lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)" |
641 lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)" |
642 by iprover |
642 by iprover |
643 |
643 |