# HG changeset patch
# User wenzelm
# Date 1727639867 -7200
# Node ID 6d34c2bedaa3835be1a5985c408a8d2ec19472ff
# Parent  5ea48342e0ae9bb8efcd66e6f36e77d01aa4c135
clarified markup: avoid conflict of "notation" with "entity", e.g. in "[x,y,z]" without spaces;

diff -r 5ea48342e0ae -r 6d34c2bedaa3 src/CCL/Set.thy
--- a/src/CCL/Set.thy	Sun Sep 29 21:40:37 2024 +0200
+++ b/src/CCL/Set.thy	Sun Sep 29 21:57:47 2024 +0200
@@ -20,7 +20,7 @@
 syntax
   "_Coll" :: "[idt, o] \<Rightarrow> 'a set"  (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{_./ _})\<close>)
 syntax_consts
-  "_Coll" == Collect
+  Collect
 translations
   "{x. P}" == "CONST Collect(\<lambda>x. P)"
 
diff -r 5ea48342e0ae -r 6d34c2bedaa3 src/CCL/Term.thy
--- a/src/CCL/Term.thy	Sun Sep 29 21:40:37 2024 +0200
+++ b/src/CCL/Term.thy	Sun Sep 29 21:57:47 2024 +0200
@@ -51,7 +51,7 @@
 
 syntax "_let1" :: "[idt,i,i]\<Rightarrow>i"
   (\<open>(\<open>indent=3 notation=\<open>mixfix let be in\<close>\<close>let _ be _/ in _)\<close> [0,0,60] 60)
-syntax_consts "_let1" == let1
+syntax_consts let1
 translations "let x be a in e" == "CONST let1(a, \<lambda>x. e)"
 
 definition letrec :: "[[i,i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
@@ -73,10 +73,7 @@
     (\<open>(\<open>indent=3 notation=\<open>mixfix letrec be in\<close>\<close>letrec _ _ _ be _/ in _)\<close> [0,0,0,0,60] 60)
   "_letrec3" :: "[idt,idt,idt,idt,i,i]\<Rightarrow>i"
     (\<open>(\<open>indent=3 notation=\<open>mixfix letrec be in\<close>\<close>letrec _ _ _ _ be _/ in _)\<close> [0,0,0,0,0,60] 60)
-syntax_consts
-  "_letrec" == letrec and
-  "_letrec2" == letrec2 and
-  "_letrec3" == letrec3
+syntax_consts letrec letrec2 letrec3
 parse_translation \<open>
   let
     fun abs_tr t u = Syntax_Trans.abs_tr [t, u];
diff -r 5ea48342e0ae -r 6d34c2bedaa3 src/CCL/Type.thy
--- a/src/CCL/Type.thy	Sun Sep 29 21:40:37 2024 +0200
+++ b/src/CCL/Type.thy	Sun Sep 29 21:57:47 2024 +0200
@@ -15,7 +15,7 @@
 syntax
   "_Subtype" :: "[idt, 'a set, o] \<Rightarrow> 'a set"  (\<open>(\<open>indent=1 notation=\<open>mixfix Subtype\<close>\<close>{_: _ ./ _})\<close>)
 syntax_consts
-  "_Subtype" == Subtype
+  Subtype
 translations
   "{x: A. B}" == "CONST Subtype(A, \<lambda>x. B)"
 
diff -r 5ea48342e0ae -r 6d34c2bedaa3 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Sun Sep 29 21:40:37 2024 +0200
+++ b/src/FOL/IFOL.thy	Sun Sep 29 21:57:47 2024 +0200
@@ -747,7 +747,8 @@
   ""            :: \<open>letbind => letbinds\<close>              (\<open>_\<close>)
   "_binds"      :: \<open>[letbind, letbinds] => letbinds\<close>  (\<open>_;/ _\<close>)
   "_Let"        :: \<open>[letbinds, 'a] => 'a\<close>  (\<open>(\<open>notation=\<open>mixfix let in\<close>\<close>let (_)/ in (_))\<close> 10)
-syntax_consts "_Let" \<rightleftharpoons> Let
+syntax_consts
+  Let
 translations
   "_Let(_binds(b, bs), e)"  == "_Let(b, _Let(bs, e))"
   "let x = a in e"          == "CONST Let(a, \<lambda>x. e)"
diff -r 5ea48342e0ae -r 6d34c2bedaa3 src/ZF/Induct/Multiset.thy
--- a/src/ZF/Induct/Multiset.thy	Sun Sep 29 21:40:37 2024 +0200
+++ b/src/ZF/Induct/Multiset.thy	Sun Sep 29 21:57:47 2024 +0200
@@ -75,7 +75,8 @@
 
 syntax
   "_MColl" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix MCollect\<close>\<close>{# _ \<in> _./ _#})\<close>)
-syntax_consts "_MColl" \<rightleftharpoons> MCollect
+syntax_consts
+  MCollect
 translations
   "{#x \<in> M. P#}" == "CONST MCollect(M, \<lambda>x. P)"
 
diff -r 5ea48342e0ae -r 6d34c2bedaa3 src/ZF/List.thy
--- a/src/ZF/List.thy	Sun Sep 29 21:40:37 2024 +0200
+++ b/src/ZF/List.thy	Sun Sep 29 21:57:47 2024 +0200
@@ -19,9 +19,9 @@
 syntax
   "" :: "i \<Rightarrow> list_args"  (\<open>_\<close>)
   "_List_args" :: "[i, list_args] \<Rightarrow> list_args"  (\<open>_,/ _\<close>)
-  "_List" :: "list_args \<Rightarrow> i"  (\<open>[(_)]\<close>)
+  "_List" :: "list_args \<Rightarrow> i"  (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
 syntax_consts
-  "_List_args" "_List" \<rightleftharpoons> Cons
+  Cons
 translations
   "[x, xs]"     == "CONST Cons(x, [xs])"
   "[x]"         == "CONST Cons(x, [])"
diff -r 5ea48342e0ae -r 6d34c2bedaa3 src/ZF/ZF_Base.thy
--- a/src/ZF/ZF_Base.thy	Sun Sep 29 21:40:37 2024 +0200
+++ b/src/ZF/ZF_Base.thy	Sun Sep 29 21:57:47 2024 +0200
@@ -57,7 +57,7 @@
 syntax
   "_Replace" :: "[pttrn, pttrn, i, o] \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix Replace\<close>\<close>{_ ./ _ \<in> _, _})\<close>)
 syntax_consts
-  "_Replace" \<rightleftharpoons> Replace
+  Replace
 translations
   "{y. x\<in>A, Q}" \<rightleftharpoons> "CONST Replace(A, \<lambda>x y. Q)"
 
@@ -70,7 +70,7 @@
 syntax
   "_RepFun" :: "[i, pttrn, i] \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix RepFun\<close>\<close>{_ ./ _ \<in> _})\<close> [51,0,51])
 syntax_consts
-  "_RepFun" \<rightleftharpoons> RepFun
+  RepFun
 translations
   "{b. x\<in>A}" \<rightleftharpoons> "CONST RepFun(A, \<lambda>x. b)"
 
@@ -82,7 +82,7 @@
 syntax
   "_Collect" :: "[pttrn, i, o] \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{_ \<in> _ ./ _})\<close>)
 syntax_consts
-  "_Collect" \<rightleftharpoons> Collect
+  Collect
 translations
   "{x\<in>A. P}" \<rightleftharpoons> "CONST Collect(A, \<lambda>x. P)"
 
@@ -133,9 +133,9 @@
 syntax
   "" :: "i \<Rightarrow> finset_args"  (\<open>_\<close>)
   "_Finset_args" :: "[i, finset_args] \<Rightarrow> finset_args"  (\<open>_,/ _\<close>)
-  "_Finset" :: "finset_args \<Rightarrow> i"  (\<open>{(_)}\<close>)
+  "_Finset" :: "finset_args \<Rightarrow> i"  (\<open>{(\<open>notation=\<open>mixfix set enumeration\<close>\<close>_)}\<close>)
 syntax_consts
-  "_Finset_args" "_Finset" == cons
+  cons
 translations
   "{x, xs}" == "CONST cons(x, {xs})"
   "{x}" == "CONST cons(x, 0)"
@@ -196,9 +196,9 @@
 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\<close>\<close>_,/ _)\<rangle>\<close>)
+  "_Tuple" :: "[i, tuple_args] \<Rightarrow> i"              (\<open>\<langle>(\<open>notation=\<open>mixfix tuple enumeration\<close>\<close>_,/ _)\<rangle>\<close>)
 syntax_consts
-  "_Tuple_args" "_Tuple" == Pair
+  Pair
 translations
   "\<langle>x, y, z\<rangle>"   == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
   "\<langle>x, y\<rangle>"      == "CONST Pair(x, y)"
diff -r 5ea48342e0ae -r 6d34c2bedaa3 src/ZF/func.thy
--- a/src/ZF/func.thy	Sun Sep 29 21:40:37 2024 +0200
+++ b/src/ZF/func.thy	Sun Sep 29 21:57:47 2024 +0200
@@ -452,7 +452,8 @@
   ""            :: "updbind \<Rightarrow> updbinds"             (\<open>_\<close>)
   "_updbinds"   :: "[updbind, updbinds] \<Rightarrow> updbinds" (\<open>_,/ _\<close>)
   "_Update"     :: "[i, updbinds] \<Rightarrow> i"              (\<open>_/'((_)')\<close> [900,0] 900)
-syntax_consts "_Update" "_updbind" \<rightleftharpoons> update
+syntax_consts
+  update
 translations
   "_Update (f, _updbinds(b,bs))"  == "_Update (_Update(f,b), bs)"
   "f(x:=y)"                       == "CONST update(f,x,y)"