# HG changeset patch
# User wenzelm
# Date 1728555624 -7200
# Node ID c9f1e926d4ed54a13e3398f58a66200db7272bb3
# Parent  6e6766cddf734e86cba1eec1e3dd07ea8144b63e
clarified inner-syntax markup;

diff -r 6e6766cddf73 -r c9f1e926d4ed src/CCL/Set.thy
--- a/src/CCL/Set.thy	Thu Oct 10 12:19:50 2024 +0200
+++ b/src/CCL/Set.thy	Thu Oct 10 12:20:24 2024 +0200
@@ -100,7 +100,7 @@
 definition mono :: "['a set \<Rightarrow> 'b set] \<Rightarrow> o"
   where "mono(f) == (ALL A B. A <= B \<longrightarrow> f(A) <= f(B))"
 
-definition singleton :: "'a \<Rightarrow> 'a set"  (\<open>{_}\<close>)
+definition singleton :: "'a \<Rightarrow> 'a set"  (\<open>(\<open>open_block notation=\<open>mixfix singleton\<close>\<close>{_})\<close>)
   where "{a} == {x. x=a}"
 
 definition empty :: "'a set"  (\<open>{}\<close>)
diff -r 6e6766cddf73 -r c9f1e926d4ed src/CCL/Term.thy
--- a/src/CCL/Term.thy	Thu Oct 10 12:19:50 2024 +0200
+++ b/src/CCL/Term.thy	Thu Oct 10 12:20:24 2024 +0200
@@ -131,7 +131,7 @@
 definition nrec :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
   where "nrec(n,b,c) == letrec g x be ncase(x, b, \<lambda>y. c(y,g(y))) in g(n)"
 
-definition nil :: "i"  (\<open>([])\<close>)
+definition nil :: "i"  (\<open>[]\<close>)
   where "[] == inl(one)"
 
 definition cons :: "[i,i]\<Rightarrow>i"  (infixr \<open>$\<close> 80)
diff -r 6e6766cddf73 -r c9f1e926d4ed src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Thu Oct 10 12:19:50 2024 +0200
+++ b/src/FOL/IFOL.thy	Thu Oct 10 12:20:24 2024 +0200
@@ -114,7 +114,7 @@
 
 notation (ASCII)
   not_equal  (infixl \<open>~=\<close> 50) and
-  Not  (\<open>~ _\<close> [40] 40) and
+  Not  (\<open>(\<open>open_block notation=\<open>prefix ~\<close>\<close>~ _)\<close> [40] 40) and
   conj  (infixr \<open>&\<close> 35) and
   disj  (infixr \<open>|\<close> 30) and
   All  (binder \<open>ALL \<close> 10) and
@@ -743,10 +743,10 @@
   where \<open>Let(s, f) \<equiv> f(s)\<close>
 
 syntax
-  "_bind"       :: \<open>[pttrn, 'a] => letbind\<close>  (\<open>(\<open>indent=2 notation=\<open>infix letbind\<close>\<close>_ =/ _)\<close> 10)
+  "_bind"       :: \<open>[pttrn, 'a] => letbind\<close>  (\<open>(\<open>indent=2 notation=\<open>infix let binding\<close>\<close>_ =/ _)\<close> 10)
   ""            :: \<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)
+  "_Let"        :: \<open>[letbinds, 'a] => 'a\<close>  (\<open>(\<open>notation=\<open>mixfix let expression\<close>\<close>let (_)/ in (_))\<close> 10)
 translations
   "_Let(_binds(b, bs), e)"  == "_Let(b, _Let(bs, e))"
   "let x = a in e"          == "CONST Let(a, \<lambda>x. e)"