# HG changeset patch
# User huffman
# Date 1289423322 28800
# Node ID 5718fb91d2d8821dca7dc39be454c65788843186
# Parent  d2e876d6da8c6d9288ec66edc40eabbc86e0e20e
removed unused lemma chain_mono2

diff -r d2e876d6da8c -r 5718fb91d2d8 src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Wed Nov 10 11:42:35 2010 -0800
+++ b/src/HOLCF/Pcpo.thy	Wed Nov 10 13:08:42 2010 -0800
@@ -238,9 +238,6 @@
 lemma notUU_I: "\<lbrakk>x \<sqsubseteq> y; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> y \<noteq> \<bottom>"
   by (blast intro: UU_I)
 
-lemma chain_mono2: "\<lbrakk>\<exists>j. Y j \<noteq> \<bottom>; chain Y\<rbrakk> \<Longrightarrow> \<exists>j. \<forall>i>j. Y i \<noteq> \<bottom>"
-  by (blast dest: notUU_I chain_mono_less)
-
 end
 
 subsection {* Chain-finite and flat cpos *}