# HG changeset patch
# User haftmann
# Date 1190299050 -7200
# Node ID 49adbdcc52e2ec72cc0d60600d0804815442f22f
# Parent  185502d54c3de8c443ebbc2e9cfd038c03cb7989
clarified code lemmas

diff -r 185502d54c3d -r 49adbdcc52e2 src/HOL/Set.thy
--- 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 *}