src/HOLCF/Deflation.thy

   apply (rule monofun_cfun_arg)
   apply (erule ep_pair.e_p_less)
  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
 
 lemma e_strict [simp]: "e\<cdot>\<bottom> = \<bottom>"