--- 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>)
--- 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)
--- 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)"