# HG changeset patch
# User wenzelm
# Date 1727729865 -7200
# Node ID 8042869c2072f3b80952b252dcd128c78466d079
# Parent  dd59daa3c37a88430595f9a989596da14fe91bad
clarified syntax: prefer nonterminal "args", use outer block (with indent);

diff -r dd59daa3c37a -r 8042869c2072 src/HOL/HOLCF/ConvexPD.thy
--- a/src/HOL/HOLCF/ConvexPD.thy	Mon Sep 30 20:30:59 2024 +0200
+++ b/src/HOL/HOLCF/ConvexPD.thy	Mon Sep 30 22:57:45 2024 +0200
@@ -178,13 +178,10 @@
     (infixl \<open>\<union>\<natural>\<close> 65) where
   "xs \<union>\<natural> ys == convex_plus\<cdot>xs\<cdot>ys"
 
-nonterminal convex_pd_args
 syntax
-  "" :: "logic \<Rightarrow> convex_pd_args"  (\<open>_\<close>)
-  "_convex_pd_args" :: "logic \<Rightarrow> convex_pd_args \<Rightarrow> convex_pd_args"  (\<open>_,/ _\<close>)
-  "_convex_pd" :: "convex_pd_args \<Rightarrow> logic"  (\<open>{_}\<natural>\<close>)
+  "_convex_pd" :: "args \<Rightarrow> logic"  (\<open>(\<open>indent=1 notation=\<open>mixfix convex_pd enumeration\<close>\<close>{_}\<natural>)\<close>)
 syntax_consts
-  "_convex_pd_args" "_convex_pd" == convex_add
+  convex_add
 translations
   "{x,xs}\<natural>" == "{x}\<natural> \<union>\<natural> {xs}\<natural>"
   "{x}\<natural>" == "CONST convex_unit\<cdot>x"
diff -r dd59daa3c37a -r 8042869c2072 src/HOL/HOLCF/IOA/Sequence.thy
--- a/src/HOL/HOLCF/IOA/Sequence.thy	Mon Sep 30 20:30:59 2024 +0200
+++ b/src/HOL/HOLCF/IOA/Sequence.thy	Mon Sep 30 22:57:45 2024 +0200
@@ -70,8 +70,8 @@
 subsection \<open>List enumeration\<close>
 
 syntax
-  "_totlist" :: "args \<Rightarrow> 'a Seq"  (\<open>[(\<open>notation=\<open>mixfix total list enumeration\<close>\<close>_)!]\<close>)
-  "_partlist" :: "args \<Rightarrow> 'a Seq"  (\<open>[(\<open>notation=\<open>mixfix partial list enumeration\<close>\<close>_)?]\<close>)
+  "_totlist" :: "args \<Rightarrow> 'a Seq"  (\<open>(\<open>indent=1 notation=\<open>mixfix total list enumeration\<close>\<close>[_!])\<close>)
+  "_partlist" :: "args \<Rightarrow> 'a Seq"  (\<open>(\<open>indent=1 notation=\<open>mixfix partial list enumeration\<close>\<close>[_?])\<close>)
 syntax_consts
   Consq
 translations
diff -r dd59daa3c37a -r 8042869c2072 src/HOL/HOLCF/LowerPD.thy
--- a/src/HOL/HOLCF/LowerPD.thy	Mon Sep 30 20:30:59 2024 +0200
+++ b/src/HOL/HOLCF/LowerPD.thy	Mon Sep 30 22:57:45 2024 +0200
@@ -133,13 +133,10 @@
     (infixl \<open>\<union>\<flat>\<close> 65) where
   "xs \<union>\<flat> ys == lower_plus\<cdot>xs\<cdot>ys"
 
-nonterminal lower_pd_args
 syntax
-  "" :: "logic \<Rightarrow> lower_pd_args"  (\<open>_\<close>)
-  "_lower_pd_args" :: "logic \<Rightarrow> lower_pd_args \<Rightarrow> lower_pd_args"  (\<open>_,/ _\<close>)
-  "_lower_pd" :: "lower_pd_args \<Rightarrow> logic" (\<open>{_}\<flat>\<close>)
+  "_lower_pd" :: "args \<Rightarrow> logic"  (\<open>(\<open>indent=1 notation=\<open>mixfix lower_pd enumeration\<close>\<close>{_}\<flat>)\<close>)
 syntax_consts
-  "_lower_pd_args" "_lower_pd" == lower_add
+  lower_add
 translations
   "{x,xs}\<flat>" == "{x}\<flat> \<union>\<flat> {xs}\<flat>"
   "{x}\<flat>" == "CONST lower_unit\<cdot>x"
diff -r dd59daa3c37a -r 8042869c2072 src/HOL/HOLCF/UpperPD.thy
--- a/src/HOL/HOLCF/UpperPD.thy	Mon Sep 30 20:30:59 2024 +0200
+++ b/src/HOL/HOLCF/UpperPD.thy	Mon Sep 30 22:57:45 2024 +0200
@@ -131,13 +131,10 @@
     (infixl \<open>\<union>\<sharp>\<close> 65) where
   "xs \<union>\<sharp> ys == upper_plus\<cdot>xs\<cdot>ys"
 
-nonterminal upper_pd_args
 syntax
-  "" :: "logic \<Rightarrow> upper_pd_args"  (\<open>_\<close>)
-  "_upper_pd_args" :: "logic \<Rightarrow> upper_pd_args \<Rightarrow> upper_pd_args"  (\<open>_,/ _\<close>)
-  "_upper_pd" :: "upper_pd_args \<Rightarrow> logic"  (\<open>{_}\<sharp>\<close>)
+  "_upper_pd" :: "args \<Rightarrow> logic"  (\<open>(\<open>indent=1 notation=\<open>mixfix upper_pd enumeration\<close>\<close>{_}\<sharp>)\<close>)
 syntax_consts
-  "_upper_pd_args" "_upper_pd" == upper_add
+  upper_add
 translations
   "{x,xs}\<sharp>" == "{x}\<sharp> \<union>\<sharp> {xs}\<sharp>"
   "{x}\<sharp>" == "CONST upper_unit\<cdot>x"