diff -r ff27dc6e7d05 -r 4a7415c67063 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Tue Jun 10 15:30:56 2008 +0200
+++ b/src/HOL/Orderings.thy	Tue Jun 10 15:30:58 2008 +0200
@@ -103,6 +103,28 @@
 by (rule less_asym)
 
 
+text {* Least value operator *}
+
+definition
+  Least :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "LEAST " 10) where
+  "Least P = (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> x \<le> y))"
+
+lemma Least_equality:
+  assumes "P x"
+    and "\<And>y. P y \<Longrightarrow> x \<le> y"
+  shows "Least P = x"
+unfolding Least_def by (rule the_equality)
+  (blast intro: assms antisym)+
+
+lemma LeastI2_order:
+  assumes "P x"
+    and "\<And>y. P y \<Longrightarrow> x \<le> y"
+    and "\<And>x. P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> x \<le> y \<Longrightarrow> Q x"
+  shows "Q (Least P)"
+unfolding Least_def by (rule theI2)
+  (blast intro: assms antisym)+
+
+
 text {* Dual order *}
 
 lemma dual_order:
@@ -1052,16 +1074,6 @@
 
 end
 
-lemma LeastI2_order:
-  "[| P (x::'a::order);
-      !!y. P y ==> x <= y;
-      !!x. [| P x; ALL y. P y --> x \<le> y |] ==> Q x |]
-   ==> Q (Least P)"
-apply (unfold Least_def)
-apply (rule theI2)
-  apply (blast intro: order_antisym)+
-done
-
 lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
 by (simp add: min_def)