--- a/src/FOL/IFOL.thy Mon Dec 03 21:02:26 2001 +0100
+++ b/src/FOL/IFOL.thy Mon Dec 03 21:03:06 2001 +0100
@@ -117,7 +117,7 @@
setup Simplifier.setup
use "IFOL_lemmas.ML"
-declare impE [Pure.elim] iffD1 [Pure.elim] iffD2 [Pure.elim]
+declare impE [Pure.elim?] iffD1 [Pure.elim?] iffD2 [Pure.elim?]
use "fologic.ML"
use "hypsubstdata.ML"
@@ -125,6 +125,37 @@
use "intprover.ML"
+lemma impE':
+ (assumes 1: "P --> Q" and 2: "Q ==> R" and 3: "P --> Q ==> P") R
+proof -
+ from 3 and 1 have P .
+ with 1 have Q ..
+ with 2 show R .
+qed
+
+lemma allE':
+ (assumes 1: "ALL x. P(x)" and 2: "P(x) ==> ALL x. P(x) ==> Q") Q
+proof -
+ from 1 have "P(x)" by (rule spec)
+ from this and 1 show Q by (rule 2)
+qed
+
+lemma notE': (assumes 1: "~ P" and 2: "~ P ==> P") R
+proof -
+ from 2 and 1 have P .
+ with 1 show R by (rule notE)
+qed
+
+lemmas [Pure.elim!] = disjE iffE FalseE conjE exE
+ and [Pure.intro!] = iffI conjI impI TrueI notI allI refl
+ and [Pure.elim 2] = allE notE' impE'
+ and [Pure.intro] = exI disjI2 disjI1
+
+ML_setup {*
+ Context.>> (RuleContext.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac));
+*}
+
+
subsection {* Atomizing meta-level rules *}
lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
@@ -191,6 +222,6 @@
mp
trans
-lemmas [Pure.elim] = sym
+lemmas [Pure.elim?] = sym
end