# 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': "\directed S; S <<| x\ \ (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 \ Ibottom \ Iup (THE a. Iup a = z) = z"