# HG changeset patch
# User slotosch
# Date 859380245 -3600
# Node ID 7e03e61612b0d5fa78ee9debccdca3fac66d2821
# Parent  7ca787c6efcaef499eeabe7221ce0906fab97aed
generalized theorems and class instances for Cprod.
Now "*"::(cpo,cpo)cpo and "*"::(pcpo,pcpo)pcpo

diff -r 7ca787c6efca -r 7e03e61612b0 src/HOLCF/Cprod1.thy
--- a/src/HOLCF/Cprod1.thy	Tue Mar 25 11:19:09 1997 +0100
+++ b/src/HOLCF/Cprod1.thy	Wed Mar 26 13:44:05 1997 +0100
@@ -10,6 +10,8 @@
 
 Cprod1 = Cfun3 +
 
+default cpo
+
 defs
 
   less_cprod_def "less p1 p2 == (fst p1<<fst p2 & snd p1 << snd p2)"
diff -r 7ca787c6efca -r 7e03e61612b0 src/HOLCF/Cprod2.ML
--- a/src/HOLCF/Cprod2.ML	Tue Mar 25 11:19:09 1997 +0100
+++ b/src/HOLCF/Cprod2.ML	Wed Mar 26 13:44:05 1997 +0100
@@ -147,7 +147,7 @@
 
 *)
 
-qed_goal "cpo_cprod" thy "is_chain(S::nat=>'a*'b)==>? x.range S<<| x"
+qed_goal "cpo_cprod" thy "is_chain(S::nat=>'a::cpo*'b::cpo)==>? x.range S<<| x"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r 7ca787c6efca -r 7e03e61612b0 src/HOLCF/Cprod2.thy
--- a/src/HOLCF/Cprod2.thy	Tue Mar 25 11:19:09 1997 +0100
+++ b/src/HOLCF/Cprod2.thy	Wed Mar 26 13:44:05 1997 +0100
@@ -9,7 +9,9 @@
 
 Cprod2 = Cprod1 + 
 
-instance "*"::(pcpo,pcpo)po 
+default pcpo
+
+instance "*"::(cpo,cpo)po 
 	(refl_less_cprod,antisym_less_cprod,trans_less_cprod)
 end
 
diff -r 7ca787c6efca -r 7e03e61612b0 src/HOLCF/Cprod3.ML
--- a/src/HOLCF/Cprod3.ML	Tue Mar 25 11:19:09 1997 +0100
+++ b/src/HOLCF/Cprod3.ML	Wed Mar 26 13:44:05 1997 +0100
@@ -20,8 +20,8 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "Cprod3_lemma1" Cprod3.thy 
-"is_chain(Y::(nat=>'a)) ==>\
-\ (lub(range(Y)),(x::'b)) =\
+"is_chain(Y::(nat=>'a::cpo)) ==>\
+\ (lub(range(Y)),(x::'b::cpo)) =\
 \ (lub(range(%i. fst(Y i,x))),lub(range(%i. snd(Y i,x))))"
  (fn prems =>
         [
@@ -57,8 +57,8 @@
         ]);
 
 qed_goal "Cprod3_lemma2" Cprod3.thy 
-"is_chain(Y::(nat=>'a)) ==>\
-\ ((x::'b),lub(range Y)) =\
+"is_chain(Y::(nat=>'a::cpo)) ==>\
+\ ((x::'b::cpo),lub(range Y)) =\
 \ (lub(range(%i. fst(x,Y i))),lub(range(%i. snd(x, Y i))))"
  (fn prems =>
         [
diff -r 7ca787c6efca -r 7e03e61612b0 src/HOLCF/Cprod3.thy
--- a/src/HOLCF/Cprod3.thy	Tue Mar 25 11:19:09 1997 +0100
+++ b/src/HOLCF/Cprod3.thy	Wed Mar 26 13:44:05 1997 +0100
@@ -9,7 +9,8 @@
 
 Cprod3 = Cprod2 +
 
-instance "*" :: (pcpo,pcpo)pcpo   (least_cprod,cpo_cprod)
+instance "*" :: (cpo,cpo)cpo   	  (cpo_cprod)
+instance "*" :: (pcpo,pcpo)pcpo   (least_cprod)
 
 consts  
         cpair        :: "'a -> 'b -> ('a*'b)" (* continuous  pairing *)