src/HOL/Set.thy
changeset 27106 ff27dc6e7d05
parent 26800 dcf1dfc915a7
child 27418 564117b58d73
     1.1 --- a/src/HOL/Set.thy	Tue Jun 10 15:30:54 2008 +0200
     1.2 +++ b/src/HOL/Set.thy	Tue Jun 10 15:30:56 2008 +0200
     1.3 @@ -2156,7 +2156,7 @@
     1.4  definition
     1.5    contents :: "'a set \<Rightarrow> 'a"
     1.6  where
     1.7 -  "contents X = (THE x. X = {x})"
     1.8 +  [code func del]: "contents X = (THE x. X = {x})"
     1.9  
    1.10  lemma contents_eq [simp]: "contents {x} = x"
    1.11    by (simp add: contents_def)
    1.12 @@ -2202,13 +2202,6 @@
    1.13    apply (auto elim: monoD intro!: order_antisym)
    1.14    done
    1.15  
    1.16 -lemma Least_equality:
    1.17 -  "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"
    1.18 -apply (simp add: Least_def)
    1.19 -apply (rule the_equality)
    1.20 -apply (auto intro!: order_antisym)
    1.21 -done
    1.22 -
    1.23  
    1.24  subsection {* Basic ML bindings *}
    1.25