src/HOL/Set.thy
changeset 18144 4edcb5fdc3b0
parent 17875 d81094515061
child 18315 e52f867ab851
     1.1 --- a/src/HOL/Set.thy	Thu Nov 10 17:31:44 2005 +0100
     1.2 +++ b/src/HOL/Set.thy	Thu Nov 10 17:33:14 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: "A \<subseteq> A"
     1.8 +lemma subset_refl [simp,intro!]: "A \<subseteq> A"
     1.9    by fast
    1.10  
    1.11  lemma subset_trans: "A \<subseteq> B ==> B \<subseteq> C ==> A \<subseteq> C"
    1.12 @@ -600,7 +600,7 @@
    1.13  lemma UNIV_witness [intro?]: "EX x. x : UNIV"
    1.14    by simp
    1.15  
    1.16 -lemma subset_UNIV: "A \<subseteq> UNIV"
    1.17 +lemma subset_UNIV [simp]: "A \<subseteq> UNIV"
    1.18    by (rule subsetI) (rule UNIV_I)
    1.19  
    1.20  text {*
    1.21 @@ -980,8 +980,6 @@
    1.22    change_simpset (fn ss => ss setmksimps (mksimps mksimps_pairs));
    1.23  *}
    1.24  
    1.25 -declare subset_UNIV [simp] subset_refl [simp]
    1.26 -
    1.27  
    1.28  subsubsection {* The ``proper subset'' relation *}
    1.29