src/HOL/Set.thy
changeset 14479 0eca4aabf371
parent 14398 c5c47703f763
child 14551 2cb6ff394bfb
     1.1 --- a/src/HOL/Set.thy	Fri Mar 19 11:06:53 2004 +0100
     1.2 +++ b/src/HOL/Set.thy	Wed Mar 24 10:50:29 2004 +0100
     1.3 @@ -1949,6 +1949,16 @@
     1.4    by blast
     1.5  
     1.6  
     1.7 +subsection {* Getting the Contents of a Singleton Set *}
     1.8 +
     1.9 +constdefs
    1.10 +  contents :: "'a set => 'a"
    1.11 +   "contents X == THE x. X = {x}"
    1.12 +
    1.13 +lemma contents_eq [simp]: "contents {x} = x"
    1.14 +by (simp add: contents_def)
    1.15 +
    1.16 +
    1.17  subsection {* Transitivity rules for calculational reasoning *}
    1.18  
    1.19  lemma forw_subst: "a = b ==> P b ==> P a"