src/HOL/Set.thy

--- a/src/HOL/Set.thy	Thu Dec 01 08:28:02 2005 +0100
+++ b/src/HOL/Set.thy	Thu Dec 01 15:45:54 2005 +0100
@@ -524,7 +524,7 @@
 lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
   by blast
 
-lemma subset_refl [simp,intro!]: "A \<subseteq> A"
+lemma subset_refl [simp]: "A \<subseteq> A"
   by fast
 
 lemma subset_trans: "A \<subseteq> B ==> B \<subseteq> C ==> A \<subseteq> C"