# HG changeset patch
# User wenzelm
# Date 1727868843 -7200
# Node ID 8407b4c068e227588947febc6a9db36363a1a786
# Parent  6ae3d0b2b8ad8358636147100031fac449766936
clarified abbreviation;

diff -r 6ae3d0b2b8ad -r 8407b4c068e2 src/HOL/HOLCF/Pcpo.thy
--- a/src/HOL/HOLCF/Pcpo.thy	Wed Oct 02 11:27:19 2024 +0200
+++ b/src/HOL/HOLCF/Pcpo.thy	Wed Oct 02 13:34:03 2024 +0200
@@ -151,10 +151,7 @@
 end
 
 text \<open>Old "UU" syntax:\<close>
-
-syntax UU :: logic
-syntax_consts UU \<rightleftharpoons> bottom
-translations "UU" \<rightharpoonup> "CONST bottom"
+abbreviation (input) "UU \<equiv> bottom"
 
 text \<open>Simproc to rewrite \<^term>\<open>\<bottom> = x\<close> to \<^term>\<open>x = \<bottom>\<close>.\<close>
 setup \<open>Reorient_Proc.add (fn \<^Const_>\<open>bottom _\<close> => true | _ => false)\<close>