--- a/src/HOL/Set.thy Thu Sep 20 16:37:29 2007 +0200
+++ b/src/HOL/Set.thy Thu Sep 20 16:37:30 2007 +0200
@@ -2081,13 +2081,13 @@
subsection {* Getting the Contents of a Singleton Set *}
-constdefs
- contents :: "'a set => 'a"
- "contents X == THE x. X = {x}"
-lemmas [code func del] = contents_def
-
-lemma contents_eq [simp, code func]: "contents {x} = x"
-by (simp add: contents_def)
+definition
+ contents :: "'a set \<Rightarrow> 'a"
+where
+ [code func del]: "contents X = (THE x. X = {x})"
+
+lemma contents_eq [simp]: "contents {x} = x"
+ by (simp add: contents_def)
subsection {* Transitivity rules for calculational reasoning *}
@@ -2140,7 +2140,7 @@
subsubsection {* Primitive operations *}
lemma minus_insert [code func]:
- "insert a A - B = (let C = A - B in if a \<in> B then C else insert a C)"
+ "insert (a\<Colon>'a\<Colon>eq) A - B = (let C = A - B in if a \<in> B then C else insert a C)"
by (auto simp add: Let_def)
lemma minus_empty1 [code func]:
@@ -2191,6 +2191,11 @@
"UNION {} f = {}"
by auto
+lemma contents_insert [code func]:
+ "contents (insert a A) = contents (insert a (A - {a}))"
+ by auto
+declare contents_eq [code func]
+
subsubsection {* Derived predicates *}