changeset 33369 | 470a7b233ee5 |
parent 32172 | c4e55f30d527 |
child 35054 | a5db9779b026 |
--- a/src/FOL/IFOL.thy Sun Nov 01 15:24:45 2009 +0100 +++ b/src/FOL/IFOL.thy Sun Nov 01 15:44:26 2009 +0100 @@ -646,7 +646,7 @@ and [Pure.elim 2] = allE notE' impE' and [Pure.intro] = exI disjI2 disjI1 -setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac) *} +setup {* Context_Rules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac) *} lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)"