--- a/src/HOLCF/Porder.thy Thu May 26 18:34:23 2005 +0200
+++ b/src/HOLCF/Porder.thy Fri May 27 00:15:24 2005 +0200
@@ -253,6 +253,6 @@
apply (blast dest: ub_rangeD intro: is_lubI ub_rangeI)
done
-end
+lemmas thelub_const = lub_const [THEN thelubI, standard]
-
+end