equal
deleted
inserted
replaced
150 and [Pure.intro!] = iffI conjI impI TrueI notI allI refl |
150 and [Pure.intro!] = iffI conjI impI TrueI notI allI refl |
151 and [Pure.elim 2] = allE notE' impE' |
151 and [Pure.elim 2] = allE notE' impE' |
152 and [Pure.intro] = exI disjI2 disjI1 |
152 and [Pure.intro] = exI disjI2 disjI1 |
153 |
153 |
154 ML_setup {* |
154 ML_setup {* |
155 Context.>> (RuleContext.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)); |
155 Context.>> (ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac)); |
156 *} |
156 *} |
157 |
157 |
158 |
158 |
159 subsection {* Atomizing meta-level rules *} |
159 subsection {* Atomizing meta-level rules *} |
160 |
160 |