src/HOL/Set.thy
changeset 34209 c7f621786035
parent 33935 b94b4587106a
child 34974 18b41bba42b5
     1.1 --- a/src/HOL/Set.thy	Wed Dec 30 01:08:33 2009 +0100
     1.2 +++ b/src/HOL/Set.thy	Wed Dec 30 10:24:53 2009 +0100
     1.3 @@ -517,10 +517,10 @@
     1.4  *}
     1.5  
     1.6  lemma equalityD1: "A = B ==> A \<subseteq> B"
     1.7 -  by (simp add: subset_refl)
     1.8 +  by simp
     1.9  
    1.10  lemma equalityD2: "A = B ==> B \<subseteq> A"
    1.11 -  by (simp add: subset_refl)
    1.12 +  by simp
    1.13  
    1.14  text {*
    1.15    \medskip Be careful when adding this to the claset as @{text
    1.16 @@ -529,7 +529,7 @@
    1.17  *}
    1.18  
    1.19  lemma equalityE: "A = B ==> (A \<subseteq> B ==> B \<subseteq> A ==> P) ==> P"
    1.20 -  by (simp add: subset_refl)
    1.21 +  by simp
    1.22  
    1.23  lemma equalityCE [elim]:
    1.24      "A = B ==> (c \<in> A ==> c \<in> B ==> P) ==> (c \<notin> A ==> c \<notin> B ==> P) ==> P"
    1.25 @@ -629,7 +629,7 @@
    1.26    by simp
    1.27  
    1.28  lemma Pow_top: "A \<in> Pow A"
    1.29 -  by (simp add: subset_refl)
    1.30 +  by simp
    1.31  
    1.32  
    1.33  subsubsection {* Set complement *}