--- 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>)
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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