--- 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"