src/HOL/Set.thy
changeset 39910 10097e0a9dbd
parent 39302 d7728f65b353
child 40703 d1fc454d6735
     1.1 --- a/src/HOL/Set.thy	Fri Oct 01 14:15:49 2010 +0200
     1.2 +++ b/src/HOL/Set.thy	Fri Oct 01 16:05:25 2010 +0200
     1.3 @@ -1656,11 +1656,11 @@
     1.4  
     1.5  subsubsection {* Getting the Contents of a Singleton Set *}
     1.6  
     1.7 -definition contents :: "'a set \<Rightarrow> 'a" where
     1.8 -  "contents X = (THE x. X = {x})"
     1.9 +definition the_elem :: "'a set \<Rightarrow> 'a" where
    1.10 +  "the_elem X = (THE x. X = {x})"
    1.11  
    1.12 -lemma contents_eq [simp]: "contents {x} = x"
    1.13 -  by (simp add: contents_def)
    1.14 +lemma the_elem_eq [simp]: "the_elem {x} = x"
    1.15 +  by (simp add: the_elem_def)
    1.16  
    1.17  
    1.18  subsubsection {* Least value operator *}