# HG changeset patch
# User wenzelm
# Date 1724924594 -7200
# Node ID 66a8113ac23e568a7fa06ce1505c3dc6f69b8b83
# Parent  f27f66e9adcac05df35fda727a7fc0bc02ef84b7
more specific "args" syntax, to support more markup for syntax consts;

diff -r f27f66e9adca -r 66a8113ac23e src/ZF/List.thy
--- a/src/ZF/List.thy	Thu Aug 29 11:39:50 2024 +0200
+++ b/src/ZF/List.thy	Thu Aug 29 11:43:14 2024 +0200
@@ -15,9 +15,13 @@
 
 notation Nil (\<open>[]\<close>)
 
+nonterminal list_args
 syntax
- "_List" :: "is \<Rightarrow> i"  (\<open>[(_)]\<close>)
-syntax_consts "_List" \<rightleftharpoons> Cons
+  "" :: "i \<Rightarrow> list_args"  (\<open>_\<close>)
+  "_List_args" :: "[i, list_args] \<Rightarrow> list_args"  (\<open>_,/ _\<close>)
+  "_List" :: "list_args \<Rightarrow> i"  (\<open>[(_)]\<close>)
+syntax_consts
+  "_List_args" "_List" \<rightleftharpoons> Cons
 translations
   "[x, xs]"     == "CONST Cons(x, [xs])"
   "[x]"         == "CONST Cons(x, [])"
diff -r f27f66e9adca -r 66a8113ac23e src/ZF/ZF_Base.thy
--- a/src/ZF/ZF_Base.thy	Thu Aug 29 11:39:50 2024 +0200
+++ b/src/ZF/ZF_Base.thy	Thu Aug 29 11:43:14 2024 +0200
@@ -129,13 +129,13 @@
 definition succ :: "i \<Rightarrow> i"
   where "succ(i) \<equiv> cons(i, i)"
 
-nonterminal "is"
+nonterminal "finset_args"
 syntax
-  "" :: "i \<Rightarrow> is"  (\<open>_\<close>)
-  "_Enum" :: "[i, is] \<Rightarrow> is"  (\<open>_,/ _\<close>)
-  "_Finset" :: "is \<Rightarrow> i"  (\<open>{(_)}\<close>)
+  "" :: "i \<Rightarrow> finset_args"  (\<open>_\<close>)
+  "_Finset_args" :: "[i, finset_args] \<Rightarrow> finset_args"  (\<open>_,/ _\<close>)
+  "_Finset" :: "finset_args \<Rightarrow> i"  (\<open>{(_)}\<close>)
 syntax_consts
-  "_Finset" == cons
+  "_Finset_args" "_Finset" == cons
 translations
   "{x, xs}" == "CONST cons(x, {xs})"
   "{x}" == "CONST cons(x, 0)"
@@ -192,19 +192,26 @@
 definition split :: "[[i, i] \<Rightarrow> 'a, i] \<Rightarrow> 'a::{}"  \<comment> \<open>for pattern-matching\<close>
   where "split(c) \<equiv> \<lambda>p. c(fst(p), snd(p))"
 
+nonterminal "tuple_args"
+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>(_,/ _)\<rangle>\<close>)
+syntax_consts
+  "_Tuple_args" "_Tuple" == Pair
+translations
+  "\<langle>x, y, z\<rangle>"   == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
+  "\<langle>x, y\<rangle>"      == "CONST Pair(x, y)"
+
 (* Patterns -- extends pre-defined type "pttrn" used in abstractions *)
 nonterminal patterns
 syntax
   "_pattern"  :: "patterns \<Rightarrow> pttrn"         (\<open>\<langle>_\<rangle>\<close>)
   ""          :: "pttrn \<Rightarrow> patterns"         (\<open>_\<close>)
   "_patterns" :: "[pttrn, patterns] \<Rightarrow> patterns"  (\<open>_,/_\<close>)
-  "_Tuple"    :: "[i, is] \<Rightarrow> i"              (\<open>\<langle>(_,/ _)\<rangle>\<close>)
 syntax_consts
-  "_pattern" "_patterns" == split and
-  "_Tuple" == Pair
+  "_pattern" "_patterns" == split
 translations
-  "\<langle>x, y, z\<rangle>"   == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
-  "\<langle>x, y\<rangle>"      == "CONST Pair(x, y)"
   "\<lambda>\<langle>x,y,zs\<rangle>.b" == "CONST split(\<lambda>x \<langle>y,zs\<rangle>.b)"
   "\<lambda>\<langle>x,y\<rangle>.b"    == "CONST split(\<lambda>x y. b)"
 
@@ -300,7 +307,7 @@
   "_PROD"     :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(3PROD _:_./ _)\<close> 10)
   "_SUM"      :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(3SUM _:_./ _)\<close> 10)
   "_lam"      :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(3lam _:_./ _)\<close> 10)
-  "_Tuple"    :: "[i, is] \<Rightarrow> i"              (\<open><(_,/ _)>\<close>)
+  "_Tuple"    :: "[i, tuple_args] \<Rightarrow> i"      (\<open><(_,/ _)>\<close>)
   "_pattern"  :: "patterns \<Rightarrow> pttrn"         (\<open><_>\<close>)