diff -r 3683f0486a11 -r a1a481ee9425 src/HOLCF/Porder.thy
--- 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