# HG changeset patch
# User haftmann
# Date 1233004535 -3600
# Node ID 2baf1b2f6655151d608182d2b36cc5e9d586c871
# Parent  3eb52e5a90a00917e4348060459f50f132749c33
explicit constraints

diff -r 3eb52e5a90a0 -r 2baf1b2f6655 src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Mon Jan 26 22:14:51 2009 +0100
+++ b/src/HOLCF/Pcpo.thy	Mon Jan 26 22:15:35 2009 +0100
@@ -14,7 +14,7 @@
 
 class cpo = po +
         -- {* class axiom: *}
-  assumes cpo:   "chain S \<Longrightarrow> \<exists>x. range S <<| x"
+  assumes cpo:   "chain S \<Longrightarrow> \<exists>x :: 'a::po. range S <<| x"
 
 text {* in cpo's everthing equal to THE lub has lub properties for every chain *}
 
@@ -257,10 +257,10 @@
 class finite_po = finite + po
 
 class chfin = po +
-  assumes chfin: "chain Y \<Longrightarrow> \<exists>n. max_in_chain n Y"
+  assumes chfin: "chain Y \<Longrightarrow> \<exists>n. max_in_chain n (Y :: nat => 'a::po)"
 
 class flat = pcpo +
-  assumes ax_flat: "x \<sqsubseteq> y \<Longrightarrow> (x = \<bottom>) \<or> (x = y)"
+  assumes ax_flat: "(x :: 'a::pcpo) \<sqsubseteq> y \<Longrightarrow> x = \<bottom> \<or> x = y"
 
 text {* finite partial orders are chain-finite *}