src/HOL/HOLCF/IOA/Sequence.thy
changeset 81095 49c04500c5f9
parent 81091 c007e6d9941d
--- a/src/HOL/HOLCF/IOA/Sequence.thy	Tue Oct 01 22:12:11 2024 +0200
+++ b/src/HOL/HOLCF/IOA/Sequence.thy	Tue Oct 01 23:36:10 2024 +0200
@@ -63,7 +63,7 @@
               UU \<Rightarrow> UU
             | Def y \<Rightarrow> (if P y then x ## (h \<cdot> xs) else h \<cdot> xs))))"
 
-abbreviation Consq_syn  (\<open>(_/\<leadsto>_)\<close> [66, 65] 65)
+abbreviation Consq_syn  (\<open>(\<open>notation=\<open>infix \<leadsto>\<close>\<close>_/\<leadsto>_)\<close> [66, 65] 65)
   where "a \<leadsto> s \<equiv> Consq a \<cdot> s"