# HG changeset patch
# User huffman
# Date 1201919316 -3600
# Node ID 9f8810c42604fa4a9a6b24e6ab7fe4d2f215edf2
# Parent  97d00128072b11f6abb67997972f00c600a3ed9c
instance "*" :: (sq_ord, sq_ord) sq_ord

diff -r 97d00128072b -r 9f8810c42604 src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Sat Feb 02 03:26:40 2008 +0100
+++ b/src/HOLCF/Cprod.thy	Sat Feb 02 03:28:36 2008 +0100
@@ -45,13 +45,16 @@
 
 subsection {* Product type is a partial order *}
 
-instantiation "*" :: (po, po) po
+instantiation "*" :: (sq_ord, sq_ord) sq_ord
 begin
 
 definition
   less_cprod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
 
-instance
+instance ..
+end
+
+instance "*" :: (po, po) po
 proof
   fix x :: "'a \<times> 'b"
   show "x \<sqsubseteq> x"
@@ -68,8 +71,6 @@
     by (fast intro: trans_less)
 qed
 
-end
-
 subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
 
 lemma prod_lessI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"