src/HOL/HOLCF/Deflation.thy
changeset 46868 6c250adbe101
parent 42151 4da4fc77664b
child 58880 0baae4311a9f
     1.1 --- a/src/HOL/HOLCF/Deflation.thy	Sun Mar 11 13:39:16 2012 +0100
     1.2 +++ b/src/HOL/HOLCF/Deflation.thy	Sun Mar 11 13:54:08 2012 +0100
     1.3 @@ -379,9 +379,9 @@
     1.4      by simp
     1.5  qed
     1.6  
     1.7 -locale pcpo_ep_pair = ep_pair +
     1.8 -  constrains e :: "'a::pcpo \<rightarrow> 'b::pcpo"
     1.9 -  constrains p :: "'b::pcpo \<rightarrow> 'a::pcpo"
    1.10 +locale pcpo_ep_pair = ep_pair e p
    1.11 +  for e :: "'a::pcpo \<rightarrow> 'b::pcpo"
    1.12 +  and p :: "'b::pcpo \<rightarrow> 'a::pcpo"
    1.13  begin
    1.14  
    1.15  lemma e_strict [simp]: "e\<cdot>\<bottom> = \<bottom>"