--- a/src/HOL/HOLCF/ConvexPD.thy Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/HOLCF/ConvexPD.thy Wed Aug 28 22:54:45 2024 +0200
@@ -178,12 +178,13 @@
(infixl "\<union>\<natural>" 65) where
"xs \<union>\<natural> ys == convex_plus\<cdot>xs\<cdot>ys"
+nonterminal convex_pd_args
syntax
- "_convex_pd" :: "args \<Rightarrow> logic" ("{_}\<natural>")
-
+ "" :: "logic \<Rightarrow> convex_pd_args" ("_")
+ "_convex_pd_args" :: "logic \<Rightarrow> convex_pd_args \<Rightarrow> convex_pd_args" ("_,/ _")
+ "_convex_pd" :: "convex_pd_args \<Rightarrow> logic" ("{_}\<natural>")
syntax_consts
- "_convex_pd" == convex_add
-
+ "_convex_pd_args" "_convex_pd" == convex_add
translations
"{x,xs}\<natural>" == "{x}\<natural> \<union>\<natural> {xs}\<natural>"
"{x}\<natural>" == "CONST convex_unit\<cdot>x"