src/HOL/HOLCF/Representable.thy

 class predomain = predomain_syn +
   assumes predomain_ep: "ep_pair liftemb liftprj"
   assumes cast_liftdefl: "cast\<cdot>(liftdefl TYPE('a)) = liftemb oo liftprj"
 
 syntax "_LIFTDEFL" :: "type \<Rightarrow> logic"  ("(1LIFTDEFL/(1'(_')))")
+syntax_consts "_LIFTDEFL" \<rightleftharpoons> liftdefl
 translations "LIFTDEFL('t)" \<rightleftharpoons> "CONST liftdefl TYPE('t)"
 
 definition liftdefl_of :: "udom defl \<rightarrow> udom u defl"
   where "liftdefl_of = defl_fun1 ID ID u_map"
 

   assumes liftemb_eq: "liftemb = u_map\<cdot>emb"
   assumes liftprj_eq: "liftprj = u_map\<cdot>prj"
   assumes liftdefl_eq: "liftdefl TYPE('a) = liftdefl_of\<cdot>(defl TYPE('a))"
 
 syntax "_DEFL" :: "type \<Rightarrow> logic"  ("(1DEFL/(1'(_')))")
+syntax_consts "_DEFL" \<rightleftharpoons> defl
 translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)"
 
 instance "domain" \<subseteq> predomain
 proof
   show "ep_pair liftemb (liftprj::udom\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>)"