# HG changeset patch
# User wenzelm
# Date 1290785314 -3600
# Node ID 4c17bfdf6f846bfb2cffa774bc2d74403e77d867
# Parent  7f745e4b7ccec383a1da74177d1411c14e8189a2
prefer non-classical eliminations in Pure reasoning, notably "rule" steps;

diff -r 7f745e4b7cce -r 4c17bfdf6f84 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Fri Nov 26 14:40:33 2010 +0100
+++ b/src/HOL/Complete_Lattice.thy	Fri Nov 26 16:28:34 2010 +0100
@@ -528,7 +528,7 @@
   @{prop "X:C"} does not!  This rule is analogous to @{text spec}.
 *}
 
-lemma InterD [elim]: "A : Inter C ==> X:C ==> A:X"
+lemma InterD [elim, Pure.elim]: "A : Inter C ==> X:C ==> A:X"
   by auto
 
 lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R"
@@ -622,7 +622,7 @@
 lemma INT_I [intro!]: "(!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)"
   by (unfold INTER_def) blast
 
-lemma INT_D [elim]: "b : (INT x:A. B x) ==> a:A ==> b: B a"
+lemma INT_D [elim, Pure.elim]: "b : (INT x:A. B x) ==> a:A ==> b: B a"
   by auto
 
 lemma INT_E [elim]: "b : (INT x:A. B x) ==> (b: B a ==> R) ==> (a~:A ==> R) ==> R"
diff -r 7f745e4b7cce -r 4c17bfdf6f84 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Fri Nov 26 14:40:33 2010 +0100
+++ b/src/ZF/ZF.thy	Fri Nov 26 16:28:34 2010 +0100
@@ -603,7 +603,7 @@
 
 (*A "destruct" rule -- every B in C contains A as an element, but
   A\<in>B can hold when B\<in>C does not!  This rule is analogous to "spec". *)
-lemma InterD [elim]: "[| A \<in> Inter(C);  B \<in> C |] ==> A \<in> B"
+lemma InterD [elim, Pure.elim]: "[| A \<in> Inter(C);  B \<in> C |] ==> A \<in> B"
 by (unfold Inter_def, blast)
 
 (*"Classical" elimination rule -- does not require exhibiting B\<in>C *)