# 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 \Old "UU" syntax:\ - -syntax UU :: logic -syntax_consts UU \ bottom -translations "UU" \ "CONST bottom" +abbreviation (input) "UU \ bottom" text \Simproc to rewrite \<^term>\\ = x\ to \<^term>\x = \\.\ setup \Reorient_Proc.add (fn \<^Const_>\bottom _\ => true | _ => false)\