# HG changeset patch
# User huffman
# Date 1199294895 -3600
# Node ID b2874ee9081aa5df495bd0983fc4c4a2d16aae34
# Parent  2d8b845dc298761709140c060a6c1894e0cfa944
add lemma ub2ub_monofun'

diff -r 2d8b845dc298 -r b2874ee9081a src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Wed Jan 02 18:27:07 2008 +0100
+++ b/src/HOLCF/Cont.thy	Wed Jan 02 18:28:15 2008 +0100
@@ -89,6 +89,13 @@
 apply (erule ub_rangeD)
 done
 
+lemma ub2ub_monofun':
+  "\<lbrakk>monofun f; S <| u\<rbrakk> \<Longrightarrow> f ` S <| f u"
+apply (rule ub_imageI)
+apply (erule monofunE)
+apply (erule (1) is_ubD)
+done
+
 text {* monotone functions map directed sets to directed sets *}
 
 lemma dir2dir_monofun: