# HG changeset patch
# User wenzelm
# Date 1727731946 -7200
# Node ID 843dba3d307acc0e41fefa17300459e2a80abc1e
# Parent  8042869c2072f3b80952b252dcd128c78466d079
clarified syntax: use outer block (with indent);

diff -r 8042869c2072 -r 843dba3d307a src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Sep 30 22:57:45 2024 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Sep 30 23:32:26 2024 +0200
@@ -454,7 +454,7 @@
 \<close>
 (*<*)
 no_syntax
-  "_list" :: "args => 'a list"    (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
+  "_list" :: "args => 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
 (*>*)
     syntax "_list" :: "args \<Rightarrow> 'a list" (\<open>[(_)]\<close>)
 
diff -r 8042869c2072 -r 843dba3d307a src/HOL/Codegenerator_Test/Code_Lazy_Test.thy
--- a/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy	Mon Sep 30 22:57:45 2024 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy	Mon Sep 30 23:32:26 2024 +0200
@@ -24,7 +24,7 @@
 
 no_notation lazy_llist (\<open>_\<close>)
 syntax
-  "_llist" :: "args => 'a list"    (\<open>\<^bold>[(\<open>notation=\<open>mixfix lazy list enumeration\<close>\<close>_)\<^bold>]\<close>)
+  "_llist" :: "args => 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix lazy list enumeration\<close>\<close>\<^bold>[_\<^bold>])\<close>)
 syntax_consts
   lazy_llist
 translations
diff -r 8042869c2072 -r 843dba3d307a src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Mon Sep 30 22:57:45 2024 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Mon Sep 30 23:32:26 2024 +0200
@@ -349,7 +349,7 @@
 subsection \<open>List-style syntax for polynomials\<close>
 
 syntax
-  "_poly" :: "args \<Rightarrow> 'a poly"  (\<open>[:(\<open>notation=\<open>mixfix polynomial enumeration\<close>\<close>_):]\<close>)
+  "_poly" :: "args \<Rightarrow> 'a poly"  (\<open>(\<open>indent=2 notation=\<open>mixfix polynomial enumeration\<close>\<close>[:_:])\<close>)
 syntax_consts
   pCons
 translations
diff -r 8042869c2072 -r 843dba3d307a src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Mon Sep 30 22:57:45 2024 +0200
+++ b/src/HOL/Library/FSet.thy	Mon Sep 30 23:32:26 2024 +0200
@@ -165,7 +165,7 @@
   by simp
 
 syntax
-  "_fset" :: "args => 'a fset"  (\<open>{|(\<open>notation=\<open>mixfix finite set enumeration\<close>\<close>_)|}\<close>)
+  "_fset" :: "args => 'a fset"  (\<open>(\<open>indent=2 notation=\<open>mixfix finite set enumeration\<close>\<close>{|_|})\<close>)
 syntax_consts
   finsert
 translations
diff -r 8042869c2072 -r 843dba3d307a src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Sep 30 22:57:45 2024 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Sep 30 23:32:26 2024 +0200
@@ -92,7 +92,7 @@
 by (rule add_mset_in_multiset)
 
 syntax
-  "_multiset" :: "args \<Rightarrow> 'a multiset"    (\<open>{#(\<open>notation=\<open>mixfix multiset enumeration\<close>\<close>_)#}\<close>)
+  "_multiset" :: "args \<Rightarrow> 'a multiset"  (\<open>(\<open>indent=2 notation=\<open>mixfix multiset enumeration\<close>\<close>{#_#})\<close>)
 syntax_consts
   add_mset
 translations
diff -r 8042869c2072 -r 843dba3d307a src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Sep 30 22:57:45 2024 +0200
+++ b/src/HOL/List.thy	Mon Sep 30 23:32:26 2024 +0200
@@ -46,7 +46,7 @@
 text \<open>List enumeration\<close>
 
 syntax
-  "_list" :: "args => 'a list"    (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
+  "_list" :: "args => 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
 syntax_consts
   Cons
 translations
diff -r 8042869c2072 -r 843dba3d307a src/HOL/Prolog/Test.thy
--- a/src/HOL/Prolog/Test.thy	Mon Sep 30 22:57:45 2024 +0200
+++ b/src/HOL/Prolog/Test.thy	Mon Sep 30 23:32:26 2024 +0200
@@ -19,7 +19,7 @@
 text \<open>List enumeration\<close>
 
 syntax
-  "_list" :: "args => 'a list"    (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
+  "_list" :: "args => 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
 syntax_consts
   Cons
 translations
diff -r 8042869c2072 -r 843dba3d307a src/HOL/Quotient_Examples/Lift_FSet.thy
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Mon Sep 30 22:57:45 2024 +0200
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Mon Sep 30 23:32:26 2024 +0200
@@ -96,7 +96,7 @@
 end
 
 syntax
-  "_fset" :: "args => 'a fset"  (\<open>{|(\<open>notation=\<open>mixfix finite set enumeration\<close>\<close>_)|}\<close>)
+  "_fset" :: "args => 'a fset"  (\<open>(\<open>indent=2 notation=\<open>mixfix finite set enumeration\<close>\<close>{|_|})\<close>)
 syntax_consts
   fcons
 translations
diff -r 8042869c2072 -r 843dba3d307a src/HOL/Quotient_Examples/Quotient_FSet.thy
--- a/src/HOL/Quotient_Examples/Quotient_FSet.thy	Mon Sep 30 22:57:45 2024 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy	Mon Sep 30 23:32:26 2024 +0200
@@ -289,7 +289,7 @@
   is "Cons" by auto
 
 syntax
-  "_fset" :: "args => 'a fset"  (\<open>{|(\<open>notation=\<open>mixfix finite set enumeration\<close>\<close>_)|}\<close>)
+  "_fset" :: "args => 'a fset"  (\<open>(\<open>indent=2 notation=\<open>mixfix finite set enumeration\<close>\<close>{|_|})\<close>)
 syntax_consts
   insert_fset
 translations
diff -r 8042869c2072 -r 843dba3d307a src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Sep 30 22:57:45 2024 +0200
+++ b/src/HOL/Set.thy	Mon Sep 30 23:32:26 2024 +0200
@@ -144,7 +144,7 @@
   where insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
 
 syntax
-  "_Finset" :: "args \<Rightarrow> 'a set"    (\<open>{(\<open>notation=\<open>mixfix set enumeration\<close>\<close>_)}\<close>)
+  "_Finset" :: "args \<Rightarrow> 'a set"  (\<open>(\<open>indent=1 notation=\<open>mixfix set enumeration\<close>\<close>{_})\<close>)
 syntax_consts
   insert
 translations
diff -r 8042869c2072 -r 843dba3d307a src/HOL/ex/Code_Lazy_Demo.thy
--- a/src/HOL/ex/Code_Lazy_Demo.thy	Mon Sep 30 22:57:45 2024 +0200
+++ b/src/HOL/ex/Code_Lazy_Demo.thy	Mon Sep 30 23:32:26 2024 +0200
@@ -40,7 +40,7 @@
   | LCons (lhd: 'a) (ltl: "'a llist") (infixr \<open>###\<close> 65)
 
 syntax
-  "_llist" :: "args => 'a list"    (\<open>\<^bold>\<lbrakk>(\<open>notation=\<open>mixfix lazy list enumeration\<close>\<close>_)\<^bold>\<rbrakk>\<close>)
+  "_llist" :: "args => 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix lazy list enumeration\<close>\<close>\<^bold>\<lbrakk>_\<^bold>\<rbrakk>)\<close>)
 syntax_consts
   LCons
 translations
diff -r 8042869c2072 -r 843dba3d307a src/ZF/List.thy
--- a/src/ZF/List.thy	Mon Sep 30 22:57:45 2024 +0200
+++ b/src/ZF/List.thy	Mon Sep 30 23:32:26 2024 +0200
@@ -16,7 +16,7 @@
 notation Nil (\<open>[]\<close>)
 
 syntax
-  "_List" :: "is \<Rightarrow> i"  (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
+  "_List" :: "is \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
 syntax_consts
   Cons
 translations
diff -r 8042869c2072 -r 843dba3d307a src/ZF/ZF_Base.thy
--- a/src/ZF/ZF_Base.thy	Mon Sep 30 22:57:45 2024 +0200
+++ b/src/ZF/ZF_Base.thy	Mon Sep 30 23:32:26 2024 +0200
@@ -133,7 +133,7 @@
 syntax
   "" :: "i \<Rightarrow> is"  (\<open>_\<close>)
   "_Enum" :: "[i, is] \<Rightarrow> is"  (\<open>_,/ _\<close>)
-  "_Finset" :: "is \<Rightarrow> i"  (\<open>{(\<open>notation=\<open>mixfix set enumeration\<close>\<close>_)}\<close>)
+  "_Finset" :: "is \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix set enumeration\<close>\<close>{_})\<close>)
 syntax_consts
   cons
 translations
@@ -196,7 +196,7 @@
 syntax
   "" :: "i \<Rightarrow> tuple_args"  (\<open>_\<close>)
   "_Tuple_args" :: "[i, tuple_args] \<Rightarrow> tuple_args"  (\<open>_,/ _\<close>)
-  "_Tuple" :: "[i, tuple_args] \<Rightarrow> i"              (\<open>\<langle>(\<open>notation=\<open>mixfix tuple enumeration\<close>\<close>_,/ _)\<rangle>\<close>)
+  "_Tuple" :: "[i, tuple_args] \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix tuple enumeration\<close>\<close>\<langle>_,/ _\<rangle>)\<close>)
 syntax_consts
   Pair
 translations