--- a/src/HOL/Groups_List.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Groups_List.thy Mon Sep 23 21:09:23 2024 +0200
@@ -98,9 +98,9 @@
text \<open>Some syntactic sugar for summing a function over a list:\<close>
syntax (ASCII)
- "_sum_list" :: "pttrn => 'a list => 'b => 'b" (\<open>(3SUM _<-_. _)\<close> [0, 51, 10] 10)
+ "_sum_list" :: "pttrn => 'a list => 'b => 'b" (\<open>(\<open>indent=3 notation=\<open>binder SUM\<close>\<close>SUM _<-_. _)\<close> [0, 51, 10] 10)
syntax
- "_sum_list" :: "pttrn => 'a list => 'b => 'b" (\<open>(3\<Sum>_\<leftarrow>_. _)\<close> [0, 51, 10] 10)
+ "_sum_list" :: "pttrn => 'a list => 'b => 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>_\<leftarrow>_. _)\<close> [0, 51, 10] 10)
syntax_consts
"_sum_list" == sum_list
translations \<comment> \<open>Beware of argument permutation!\<close>
@@ -597,9 +597,9 @@
text \<open>Some syntactic sugar:\<close>
syntax (ASCII)
- "_prod_list" :: "pttrn => 'a list => 'b => 'b" (\<open>(3PROD _<-_. _)\<close> [0, 51, 10] 10)
+ "_prod_list" :: "pttrn => 'a list => 'b => 'b" (\<open>(\<open>indent=3 notation=\<open>binder PROD\<close>\<close>PROD _<-_. _)\<close> [0, 51, 10] 10)
syntax
- "_prod_list" :: "pttrn => 'a list => 'b => 'b" (\<open>(3\<Prod>_\<leftarrow>_. _)\<close> [0, 51, 10] 10)
+ "_prod_list" :: "pttrn => 'a list => 'b => 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_\<leftarrow>_. _)\<close> [0, 51, 10] 10)
syntax_consts
"_prod_list" \<rightleftharpoons> prod_list
translations \<comment> \<open>Beware of argument permutation!\<close>