# HG changeset patch
# User huffman
# Date 1214873429 -7200
# Node ID 95ec4bda5bb9850b89451a7ab2b30f2d181e59e4
# Parent  3154f3765cc74f3ef93cfafe803f93b54b0b92c7
remove unused lemma is_lub_Iup'

diff -r 3154f3765cc7 -r 95ec4bda5bb9 src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Tue Jul 01 02:19:53 2008 +0200
+++ b/src/HOLCF/Up.thy	Tue Jul 01 02:50:29 2008 +0200
@@ -93,22 +93,6 @@
 apply simp
 done
 
-lemma is_lub_Iup': "\<lbrakk>directed S; S <<| x\<rbrakk> \<Longrightarrow> (Iup ` S) <<| Iup x"
-apply (rule is_lubI)
-apply (rule ub_imageI)
-apply (subst Iup_less)
-apply (erule (1) is_ubD [OF is_lubD1])
-apply (case_tac u)
-apply (drule directedD1, erule exE)
-apply (drule (1) ub_imageD)
-apply simp
-apply simp
-apply (erule is_lub_lub)
-apply (rule is_ubI)
-apply (drule (1) ub_imageD)
-apply simp
-done
-
 text {* Now some lemmas about chains of @{typ "'a u"} elements *}
 
 lemma up_lemma1: "z \<noteq> Ibottom \<Longrightarrow> Iup (THE a. Iup a = z) = z"