--- a/src/HOL/Set.thy Tue Jun 10 15:30:54 2008 +0200
+++ b/src/HOL/Set.thy Tue Jun 10 15:30:56 2008 +0200
@@ -2156,7 +2156,7 @@
definition
contents :: "'a set \<Rightarrow> 'a"
where
- "contents X = (THE x. X = {x})"
+ [code func del]: "contents X = (THE x. X = {x})"
lemma contents_eq [simp]: "contents {x} = x"
by (simp add: contents_def)
@@ -2202,13 +2202,6 @@
apply (auto elim: monoD intro!: order_antisym)
done
-lemma Least_equality:
- "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"
-apply (simp add: Least_def)
-apply (rule the_equality)
-apply (auto intro!: order_antisym)
-done
-
subsection {* Basic ML bindings *}