| changeset 14476 | 758e7acdea2f |
| parent 14387 | e96d5c42c4b0 |
| child 14641 | 79b7bd936264 |
--- 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"