# HG changeset patch
# User huffman
# Date 1286482728 25200
# Node ID fdff0444fa7d0bc3b752ee3255889ad48aae8879
# Parent  b525988432e93b9aea9f539206756f91026e3f05
remove some junk that made it in by accient

diff -r b525988432e9 -r fdff0444fa7d src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Wed Oct 06 10:49:27 2010 -0700
+++ b/src/HOLCF/CompactBasis.thy	Thu Oct 07 13:18:48 2010 -0700
@@ -108,26 +108,4 @@
     by (simp add: image_Un fold1_Un2)
 qed
 
-subsection {* Lemmas for proving if-and-only-if inequalities *}
-
-lemma chain_max_below_iff:
-  assumes Y: "chain Y" shows "Y (max i j) \<sqsubseteq> x \<longleftrightarrow> Y i \<sqsubseteq> x \<and> Y j \<sqsubseteq> x"
-apply auto
-apply (erule below_trans [OF chain_mono [OF Y le_maxI1]])
-apply (erule below_trans [OF chain_mono [OF Y le_maxI2]])
-apply (simp add: max_def)
-done
-
-lemma all_ex_below_disj_iff:
-  assumes "chain X" and "chain Y"
-  shows "(\<forall>i. \<exists>j. X i \<sqsubseteq> Z j \<or> Y i \<sqsubseteq> Z j) \<longleftrightarrow>
-         (\<forall>i. \<exists>j. X i \<sqsubseteq> Z j) \<or> (\<forall>i. \<exists>j. Y i \<sqsubseteq> Z j)"
-by (metis chain_max_below_iff assms)
-
-lemma all_ex_below_conj_iff:
-  assumes "chain X" and "chain Y" and "chain Z"
-  shows "(\<forall>i. \<exists>j. X i \<sqsubseteq> Z j \<and> Y i \<sqsubseteq> Z j) \<longleftrightarrow>
-         (\<forall>i. \<exists>j. X i \<sqsubseteq> Z j) \<and> (\<forall>i. \<exists>j. Y i \<sqsubseteq> Z j)"
-oops
-
 end