# HG changeset patch
# User huffman
# Date 1117145724 -7200
# Node ID a1a481ee9425e6e07f88e7a4499fbd17abf8bf14
# Parent  3683f0486a11649e5e00b2e66b3726f993d4188d
added lemma thelub_const

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