--- a/src/HOL/HOLCF/IOA/Sequence.thy Mon Sep 30 23:32:26 2024 +0200
+++ b/src/HOL/HOLCF/IOA/Sequence.thy Tue Oct 01 20:39:16 2024 +0200
@@ -72,8 +72,6 @@
syntax
"_totlist" :: "args \<Rightarrow> 'a Seq" (\<open>(\<open>indent=1 notation=\<open>mixfix total list enumeration\<close>\<close>[_!])\<close>)
"_partlist" :: "args \<Rightarrow> 'a Seq" (\<open>(\<open>indent=1 notation=\<open>mixfix partial list enumeration\<close>\<close>[_?])\<close>)
-syntax_consts
- Consq
translations
"[x, xs!]" \<rightleftharpoons> "x \<leadsto> [xs!]"
"[x!]" \<rightleftharpoons> "x\<leadsto>nil"