# HG changeset patch
# User huffman
# Date 1206650950 -3600
# Node ID 57923fdab83ba158cb5beb0dd9eddc3256c91de4
# Parent  758c6fef7b94d0762136bd050d998859ed8c15e0
remove commented text

diff -r 758c6fef7b94 -r 57923fdab83b src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Thu Mar 27 21:21:08 2008 +0100
+++ b/src/HOLCF/CompactBasis.thy	Thu Mar 27 21:49:10 2008 +0100
@@ -383,26 +383,7 @@
 instance compact_basis :: (profinite) po
 by (rule typedef_po
     [OF type_definition_compact_basis compact_le_def])
-(*
-definition
-  compact_le :: "'a compact_basis \<Rightarrow> 'a compact_basis \<Rightarrow> bool" where
-  "compact_le = (\<lambda>x y. Rep_compact_basis x \<sqsubseteq> Rep_compact_basis y)"
 
-lemma compact_le_refl: "compact_le x x"
-unfolding compact_le_def by (rule refl_less)
-
-lemma compact_le_trans: "\<lbrakk>compact_le x y; compact_le y z\<rbrakk> \<Longrightarrow> compact_le x z"
-unfolding compact_le_def by (rule trans_less)
-
-lemma compact_le_antisym: "\<lbrakk>compact_le x y; compact_le y x\<rbrakk> \<Longrightarrow> x = y"
-unfolding compact_le_def
-apply (rule Rep_compact_basis_inject [THEN iffD1])
-apply (erule (1) antisym_less)
-done
-
-interpretation compact_le: preorder [compact_le]
-by (rule preorder.intro, rule compact_le_refl, rule compact_le_trans)
-*)
 text {* minimal compact element *}
 
 definition