# HG changeset patch
# User huffman
# Date 1291664670 28800
# Node ID 75b4ff66781cc599ab9e040bbeb15c5307fb929c
# Parent  9883d1417ce1c4ef6fce0354309cd1746c242b9d
remove unused lemmas

diff -r 9883d1417ce1 -r 75b4ff66781c src/HOL/HOLCF/Fun_Cpo.thy
--- a/src/HOL/HOLCF/Fun_Cpo.thy	Mon Dec 06 11:22:42 2010 -0800
+++ b/src/HOL/HOLCF/Fun_Cpo.thy	Mon Dec 06 11:44:30 2010 -0800
@@ -79,26 +79,6 @@
 instance "fun"  :: (type, cpo) cpo
 by intro_classes (rule exI, erule is_lub_fun)
 
-subsection {* Chain-finiteness of function space *}
-
-lemma maxinch2maxinch_lambda:
-  "(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S"
-unfolding max_in_chain_def fun_eq_iff by simp
-
-lemma maxinch_mono:
-  "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> max_in_chain j Y"
-unfolding max_in_chain_def
-proof (intro allI impI)
-  fix k
-  assume Y: "\<forall>n\<ge>i. Y i = Y n"
-  assume ij: "i \<le> j"
-  assume jk: "j \<le> k"
-  from ij jk have ik: "i \<le> k" by simp
-  from Y ij have Yij: "Y i = Y j" by simp
-  from Y ik have Yik: "Y i = Y k" by simp
-  from Yij Yik show "Y j = Y k" by auto
-qed
-
 instance "fun" :: (type, discrete_cpo) discrete_cpo
 proof
   fix f g :: "'a \<Rightarrow> 'b"