--- a/src/HOL/HOLCF/Representable.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/HOLCF/Representable.thy Sun Aug 25 21:10:01 2024 +0200
@@ -32,6 +32,7 @@
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"
@@ -51,6 +52,7 @@
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