src/HOL/Set.thy

--- a/src/HOL/Set.thy	Fri Mar 19 11:06:53 2004 +0100
+++ b/src/HOL/Set.thy	Wed Mar 24 10:50:29 2004 +0100
@@ -1949,6 +1949,16 @@
   by blast
 
 
+subsection {* Getting the Contents of a Singleton Set *}
+
+constdefs
+  contents :: "'a set => 'a"
+   "contents X == THE x. X = {x}"
+
+lemma contents_eq [simp]: "contents {x} = x"
+by (simp add: contents_def)
+
+
 subsection {* Transitivity rules for calculational reasoning *}
 
 lemma forw_subst: "a = b ==> P b ==> P a"