src/HOL/Complete_Lattice.thy
changeset 40714 4c17bfdf6f84
parent 39302 d7728f65b353
child 40872 7c556a9240de
     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"