src/ZF/equalities.thy
changeset 45602 2a858377c3d2
parent 42793 88bee9f6eec7
child 46820 c656222c4dc1
     1.1 --- a/src/ZF/equalities.thy	Sun Nov 20 17:57:09 2011 +0100
     1.2 +++ b/src/ZF/equalities.thy	Sun Nov 20 20:15:02 2011 +0100
     1.3 @@ -81,7 +81,7 @@
     1.4  
     1.5  (*A safe special case of subset elimination, adding no new variables 
     1.6    [| cons(a,B) \<subseteq> C; [| a \<in> C; B \<subseteq> C |] ==> R |] ==> R *)
     1.7 -lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE, standard]
     1.8 +lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE]
     1.9  
    1.10  lemma subset_empty_iff: "A\<subseteq>0 <-> A=0"
    1.11  by blast