src/HOL/Orderings.thy

--- a/src/HOL/Orderings.thy	Tue May 10 18:37:43 2005 +0200
+++ b/src/HOL/Orderings.thy	Wed May 11 09:50:33 2005 +0200
@@ -203,7 +203,7 @@
   "Least P == THE x. P x & (ALL y. P y --> x <= y)"
     -- {* We can no longer use LeastM because the latter requires Hilbert-AC. *}
 
-lemma LeastI2:
+lemma LeastI2_order:
   "[| P (x::'a::order);
       !!y. P y ==> x <= y;
       !!x. [| P x; ALL y. P y --> x \<le> y |] ==> Q x |]