# HG changeset patch
# User huffman
# Date 1117067081 -7200
# Node ID fca38c55c8fa0f1b3d99c11487c335d774e677a0
# Parent  ebb53ebfd4e2c09fca1db0dd7e46de4accd1782c
added defaultsort declaration, moved cpair_less to Cprod.thy

diff -r ebb53ebfd4e2 -r fca38c55c8fa src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Thu May 26 02:24:08 2005 +0200
+++ b/src/HOLCF/Ssum.thy	Thu May 26 02:24:41 2005 +0200
@@ -11,6 +11,8 @@
 imports Cprod TypedefPcpo
 begin
 
+defaultsort pcpo
+
 subsection {* Definition of strict sum type *}
 
 typedef (Ssum)  ('a, 'b) "++" (infixr 10) = 
@@ -143,12 +145,6 @@
 
 subsection {* Ordering properties of @{term sinl} and @{term sinr} *}
 
-lemma cpair_less: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')"
-apply (rule iffI)
-apply (erule less_cprod5c)
-apply (simp add: monofun_cfun)
-done
-
 lemma less_ssum4a: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
 by (simp add: less_ssum_def Rep_Ssum_sinl cpair_less)