src/HOL/Set.thy
changeset 33022 c95102496490
parent 32888 ae17e72aac80
child 33039 5018f6a76b3f
child 33044 fd0a9c794ec1
     1.1 --- a/src/HOL/Set.thy	Tue Oct 20 15:03:17 2009 +0200
     1.2 +++ b/src/HOL/Set.thy	Tue Oct 20 15:02:48 2009 +0100
     1.3 @@ -445,7 +445,7 @@
     1.4  
     1.5  subsubsection {* Subsets *}
     1.6  
     1.7 -lemma subsetI [atp, intro!]: "(\<And>x. x \<in> A \<Longrightarrow> x \<in> B) \<Longrightarrow> A \<subseteq> B"
     1.8 +lemma subsetI [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> x \<in> B) \<Longrightarrow> A \<subseteq> B"
     1.9    unfolding mem_def by (rule le_funI, rule le_boolI)
    1.10  
    1.11  text {*
    1.12 @@ -476,7 +476,7 @@
    1.13  lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
    1.14    by blast
    1.15  
    1.16 -lemma subset_refl [simp,atp]: "A \<subseteq> A"
    1.17 +lemma subset_refl [simp]: "A \<subseteq> A"
    1.18    by (fact order_refl)
    1.19  
    1.20  lemma subset_trans: "A \<subseteq> B ==> B \<subseteq> C ==> A \<subseteq> C"