# HG changeset patch
# User huffman
# Date 1120178124 -7200
# Node ID a2844e212da499f2cfc6820edb6dfeedf4287020
# Parent  d28314d2dce3b8234f73acd44d1f556f38fc4ac1
cleaned up

diff -r d28314d2dce3 -r a2844e212da4 src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Fri Jul 01 02:30:59 2005 +0200
+++ b/src/HOLCF/Pcpo.thy	Fri Jul 01 02:35:24 2005 +0200
@@ -239,8 +239,7 @@
 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::nat. Y j \<noteq> \<bottom>; chain Y\<rbrakk> \<Longrightarrow> \<exists>j. \<forall>i>j. Y i \<noteq> \<bottom>"
+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)
 
 subsection {* Chain-finite and flat cpos *}
@@ -286,7 +285,7 @@
 instance flat < chfin
 by intro_classes (rule flat_imp_chfin)
 
-text {* flat subclass of chfin @{text "-->"} @{text adm_flat} not needed *}
+text {* flat subclass of chfin; @{text adm_flat} not needed *}
 
 lemma flat_eq: "(a::'a::flat) \<noteq> \<bottom> \<Longrightarrow> a \<sqsubseteq> b = (a = b)"
 by (safe dest!: ax_flat [rule_format])