more markup;
authorwenzelm
Wed, 25 Sep 2024 13:20:24 +0200
changeset 80953 501f55047387
parent 80952 a61ed25ba155
child 80954 47eb251187d6
more markup;
src/ZF/ZF_Base.thy
--- a/src/ZF/ZF_Base.thy	Wed Sep 25 12:59:43 2024 +0200
+++ b/src/ZF/ZF_Base.thy	Wed Sep 25 13:20:24 2024 +0200
@@ -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>(_,/ _)\<rangle>\<close>)
+  "_Tuple" :: "[i, tuple_args] \<Rightarrow> i"              (\<open>\<langle>(\<open>notation=\<open>mixfix tuple\<close>\<close>_,/ _)\<rangle>\<close>)
 syntax_consts
   "_Tuple_args" "_Tuple" == Pair
 translations