prefer non-classical eliminations in Pure reasoning, notably "rule" steps;
authorwenzelm
Fri Nov 26 16:28:34 2010 +0100 (2010-11-26)
changeset 407144c17bfdf6f84
parent 40713 7f745e4b7cce
child 40715 3ba17f07b23c
prefer non-classical eliminations in Pure reasoning, notably "rule" steps;
src/HOL/Complete_Lattice.thy
src/ZF/ZF.thy
     1.1 --- a/src/HOL/Complete_Lattice.thy	Fri Nov 26 14:40:33 2010 +0100
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Fri Nov 26 16:28:34 2010 +0100
     1.3 @@ -528,7 +528,7 @@
     1.4    @{prop "X:C"} does not!  This rule is analogous to @{text spec}.
     1.5  *}
     1.6  
     1.7 -lemma InterD [elim]: "A : Inter C ==> X:C ==> A:X"
     1.8 +lemma InterD [elim, Pure.elim]: "A : Inter C ==> X:C ==> A:X"
     1.9    by auto
    1.10  
    1.11  lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R"
    1.12 @@ -622,7 +622,7 @@
    1.13  lemma INT_I [intro!]: "(!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)"
    1.14    by (unfold INTER_def) blast
    1.15  
    1.16 -lemma INT_D [elim]: "b : (INT x:A. B x) ==> a:A ==> b: B a"
    1.17 +lemma INT_D [elim, Pure.elim]: "b : (INT x:A. B x) ==> a:A ==> b: B a"
    1.18    by auto
    1.19  
    1.20  lemma INT_E [elim]: "b : (INT x:A. B x) ==> (b: B a ==> R) ==> (a~:A ==> R) ==> R"
     2.1 --- a/src/ZF/ZF.thy	Fri Nov 26 14:40:33 2010 +0100
     2.2 +++ b/src/ZF/ZF.thy	Fri Nov 26 16:28:34 2010 +0100
     2.3 @@ -603,7 +603,7 @@
     2.4  
     2.5  (*A "destruct" rule -- every B in C contains A as an element, but
     2.6    A\<in>B can hold when B\<in>C does not!  This rule is analogous to "spec". *)
     2.7 -lemma InterD [elim]: "[| A \<in> Inter(C);  B \<in> C |] ==> A \<in> B"
     2.8 +lemma InterD [elim, Pure.elim]: "[| A \<in> Inter(C);  B \<in> C |] ==> A \<in> B"
     2.9  by (unfold Inter_def, blast)
    2.10  
    2.11  (*"Classical" elimination rule -- does not require exhibiting B\<in>C *)