
diff -r aa973ba84f69 -r 758e7acdea2f src/HOL/Real/RComplete.thy
--- a/src/HOL/Real/RComplete.thy	Fri Mar 19 10:48:22 2004 +0100
+++ b/src/HOL/Real/RComplete.thy	Fri Mar 19 10:50:06 2004 +0100
@@ -74,7 +74,7 @@
 lemma real_isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::real)"
 apply (frule isLub_isUb)
 apply (frule_tac x = y in isLub_isUb)
-apply (blast intro!: real_le_anti_sym dest!: isLub_le_isUb)
+apply (blast intro!: order_antisym dest!: isLub_le_isUb)
 done
 
 lemma real_order_restrict: "[| (x::real) <=* S'; S <= S' |] ==> x <=* S"




