src/HOL/Set.thy
changeset 19295 c5d236fe9668
parent 19277 f7602e74d948
child 19323 ec5cd5b1804c
equal deleted inserted replaced
19294:871d7aea081a 19295:c5d236fe9668
   472   by (simp add: simp_implies_def Bex_def cong: conj_cong)
   472   by (simp add: simp_implies_def Bex_def cong: conj_cong)
   473 
   473 
   474 
   474 
   475 subsubsection {* Subsets *}
   475 subsubsection {* Subsets *}
   476 
   476 
   477 lemma subsetI [intro!]: "(!!x. x:A ==> x:B) ==> A \<subseteq> B"
   477 lemma subsetI [atp,intro!]: "(!!x. x:A ==> x:B) ==> A \<subseteq> B"
   478   by (simp add: subset_def)
   478   by (simp add: subset_def)
   479 
   479 
   480 text {*
   480 text {*
   481   \medskip Map the type @{text "'a set => anything"} to just @{typ
   481   \medskip Map the type @{text "'a set => anything"} to just @{typ
   482   'a}; for overloading constants whose first argument has type @{typ
   482   'a}; for overloading constants whose first argument has type @{typ