--- a/src/HOL/HOLCF/IOA/Sequence.thy Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/HOLCF/IOA/Sequence.thy Wed Aug 28 22:54:45 2024 +0200
@@ -69,9 +69,12 @@
subsection \<open>List enumeration\<close>
+nonterminal llist_args
syntax
- "_totlist" :: "args \<Rightarrow> 'a Seq" ("[(_)!]")
- "_partlist" :: "args \<Rightarrow> 'a Seq" ("[(_)?]")
+ "" :: "'a \<Rightarrow> llist_args" ("_")
+ "_list_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args" ("_,/ _")
+ "_totlist" :: "llist_args \<Rightarrow> 'a Seq" ("[(_)!]")
+ "_partlist" :: "llist_args \<Rightarrow> 'a Seq" ("[(_)?]")
syntax_consts
"_totlist" "_partlist" \<rightleftharpoons> Consq
translations