# HG changeset patch
# User wenzelm
# Date 1007409786 -3600
# Node ID 94e812f9683e62679eb193dbcfb79e7e7c6e9447
# Parent  c3f34d7c50f8f5e480d1e1dba33b4675d185ae37
setup "rules" method;

diff -r c3f34d7c50f8 -r 94e812f9683e src/FOL/IFOL.thy
--- 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