changeset 27681 | 8cedebf55539 |
parent 27401 | 4edc81f93e35 |
child 28611 | 983c1855a7af |
--- a/src/HOLCF/Deflation.thy Fri Jul 25 12:03:31 2008 +0200 +++ b/src/HOLCF/Deflation.thy Fri Jul 25 12:03:32 2008 +0200 @@ -323,7 +323,7 @@ apply (erule ep_pair.e_p_less) done -locale (open) pcpo_ep_pair = ep_pair + +locale pcpo_ep_pair = ep_pair + constrains e :: "'a::pcpo \<rightarrow> 'b::pcpo" constrains p :: "'b::pcpo \<rightarrow> 'a::pcpo" begin