src/HOL/Real/Lubs.thy
changeset 14653 0848ab6fe5fc
parent 14368 2763da611ad9
child 15131 c69542757a4d
--- a/src/HOL/Real/Lubs.thy	Thu Apr 22 11:02:22 2004 +0200
+++ b/src/HOL/Real/Lubs.thy	Thu Apr 22 12:11:17 2004 +0200
@@ -21,12 +21,12 @@
   leastP      :: "['a =>bool,'a::ord] => bool"
     "leastP P x == (P x & x <=* Collect P)"
 
+  isUb        :: "['a set, 'a set, 'a::ord] => bool"
+    "isUb R S x   == S *<= x & x: R"
+
   isLub       :: "['a set, 'a set, 'a::ord] => bool"
     "isLub R S x  == leastP (isUb R S) x"
 
-  isUb        :: "['a set, 'a set, 'a::ord] => bool"
-    "isUb R S x   == S *<= x & x: R"
-
   ubs         :: "['a set, 'a::ord set] => 'a set"
     "ubs R S      == Collect (isUb R S)"