src/HOL/List.thy

--- a/src/HOL/List.thy	Sat Dec 14 23:48:45 2024 +0100
+++ b/src/HOL/List.thy	Sun Dec 15 14:59:57 2024 +0100
@@ -53,15 +53,17 @@
 
 open_bundle list_enumeration_syntax
 begin
+
 syntax
   "_list" :: "args \<Rightarrow> 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
-end
 syntax_consts
   "_list" \<rightleftharpoons> Cons
 translations
   "[x, xs]" \<rightleftharpoons> "x#[xs]"
   "[x]" \<rightleftharpoons> "x#[]"
 
+end
+
 
 subsection \<open>Basic list processing functions\<close>
 
@@ -90,7 +92,9 @@
 "filter P [] = []" |
 "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"
 
-text \<open>Special input syntax for filter:\<close>
+open_bundle filter_syntax  \<comment> \<open>Special input syntax for filter\<close>
+begin
+
 syntax (ASCII)
   "_filter" :: "[pttrn, 'a list, bool] => 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix filter\<close>\<close>[_<-_./ _])\<close>)
 syntax
@@ -100,6 +104,8 @@
 translations
   "[x<-xs . P]" \<rightharpoonup> "CONST filter (\<lambda>x. P) xs"
 
+end
+
 primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
 fold_Nil:  "fold f [] = id" |
 fold_Cons: "fold f (x # xs) = fold f xs \<circ> f x"
@@ -140,6 +146,9 @@
 
 nonterminal lupdbinds and lupdbind
 
+open_bundle list_update_syntax
+begin
+
 syntax
   "_lupdbind":: "['a, 'a] => lupdbind"    (\<open>(\<open>indent=2 notation=\<open>mixfix update\<close>\<close>_ :=/ _)\<close>)
   "" :: "lupdbind => lupdbinds"    (\<open>_\<close>)
@@ -152,6 +161,8 @@
   "_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs"
   "xs[i:=x]" == "CONST list_update xs i x"
 
+end
+
 primrec takeWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
 "takeWhile P [] = []" |
 "takeWhile P (x # xs) = (if P x then x # takeWhile P xs else [])"