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"