src/HOL/Set.thy
changeset 19175 c6e4b073f6a5
parent 18851 9502ce541f01
child 19233 77ca20b0ed77
     1.1 --- a/src/HOL/Set.thy	Thu Mar 02 18:49:13 2006 +0100
     1.2 +++ b/src/HOL/Set.thy	Thu Mar 02 18:50:43 2006 +0100
     1.3 @@ -522,7 +522,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]: "A \<subseteq> A"
     1.8 +lemma subset_refl [simp,atp]: "A \<subseteq> A"
     1.9    by fast
    1.10  
    1.11  lemma subset_trans: "A \<subseteq> B ==> B \<subseteq> C ==> A \<subseteq> C"