src/HOL/Set.thy
changeset 18315 e52f867ab851
parent 18144 4edcb5fdc3b0
child 18328 841261f303a1
     1.1 --- a/src/HOL/Set.thy	Thu Dec 01 08:28:02 2005 +0100
     1.2 +++ b/src/HOL/Set.thy	Thu Dec 01 15:45:54 2005 +0100
     1.3 @@ -524,7 +524,7 @@
     1.4  lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
     1.5    by blast
     1.6  
     1.7 -lemma subset_refl [simp,intro!]: "A \<subseteq> A"
     1.8 +lemma subset_refl [simp]: "A \<subseteq> A"
     1.9    by fast
    1.10  
    1.11  lemma subset_trans: "A \<subseteq> B ==> B \<subseteq> C ==> A \<subseteq> C"