diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Nominal/Examples/Class1.thy
--- a/src/HOL/Nominal/Examples/Class1.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Nominal/Examples/Class1.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -8,14 +8,14 @@
 
 text \<open>types\<close>
 
-no_notation not  ("NOT")
+no_notation not  (\<open>NOT\<close>)
 
 nominal_datatype ty =
     PR "string"
   | NOT  "ty"
-  | AND  "ty" "ty"   ("_ AND _" [100,100] 100)
-  | OR   "ty" "ty"   ("_ OR _"  [100,100] 100)
-  | IMP  "ty" "ty"   ("_ IMP _" [100,100] 100)
+  | AND  "ty" "ty"   (\<open>_ AND _\<close> [100,100] 100)
+  | OR   "ty" "ty"   (\<open>_ OR _\<close>  [100,100] 100)
+  | IMP  "ty" "ty"   (\<open>_ IMP _\<close> [100,100] 100)
 
 instantiation ty :: size
 begin
@@ -50,30 +50,30 @@
 
 nominal_datatype trm = 
     Ax   "name" "coname"
-  | Cut  "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm"            ("Cut <_>._ ('(_'))._" [0,0,0,100] 101)
-  | NotR "\<guillemotleft>name\<guillemotright>trm" "coname"                 ("NotR ('(_'))._ _" [0,100,100] 101)
-  | NotL "\<guillemotleft>coname\<guillemotright>trm" "name"                 ("NotL <_>._ _" [0,100,100] 101)
-  | AndR "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>coname\<guillemotright>trm" "coname" ("AndR <_>._ <_>._ _" [0,100,0,100,100] 101)
-  | AndL1 "\<guillemotleft>name\<guillemotright>trm" "name"                  ("AndL1 (_)._ _" [100,100,100] 101)
-  | AndL2 "\<guillemotleft>name\<guillemotright>trm" "name"                  ("AndL2 (_)._ _" [100,100,100] 101)
-  | OrR1 "\<guillemotleft>coname\<guillemotright>trm" "coname"               ("OrR1 <_>._ _" [100,100,100] 101)
-  | OrR2 "\<guillemotleft>coname\<guillemotright>trm" "coname"               ("OrR2 <_>._ _" [100,100,100] 101)
-  | OrL "\<guillemotleft>name\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name"        ("OrL (_)._ (_)._ _" [100,100,100,100,100] 101)
-  | ImpR "\<guillemotleft>name\<guillemotright>(\<guillemotleft>coname\<guillemotright>trm)" "coname"       ("ImpR (_).<_>._ _" [100,100,100,100] 101)
-  | ImpL "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name"     ("ImpL <_>._ (_)._ _" [100,100,100,100,100] 101)
+  | Cut  "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm"            (\<open>Cut <_>._ ('(_'))._\<close> [0,0,0,100] 101)
+  | NotR "\<guillemotleft>name\<guillemotright>trm" "coname"                 (\<open>NotR ('(_'))._ _\<close> [0,100,100] 101)
+  | NotL "\<guillemotleft>coname\<guillemotright>trm" "name"                 (\<open>NotL <_>._ _\<close> [0,100,100] 101)
+  | AndR "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>coname\<guillemotright>trm" "coname" (\<open>AndR <_>._ <_>._ _\<close> [0,100,0,100,100] 101)
+  | AndL1 "\<guillemotleft>name\<guillemotright>trm" "name"                  (\<open>AndL1 (_)._ _\<close> [100,100,100] 101)
+  | AndL2 "\<guillemotleft>name\<guillemotright>trm" "name"                  (\<open>AndL2 (_)._ _\<close> [100,100,100] 101)
+  | OrR1 "\<guillemotleft>coname\<guillemotright>trm" "coname"               (\<open>OrR1 <_>._ _\<close> [100,100,100] 101)
+  | OrR2 "\<guillemotleft>coname\<guillemotright>trm" "coname"               (\<open>OrR2 <_>._ _\<close> [100,100,100] 101)
+  | OrL "\<guillemotleft>name\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name"        (\<open>OrL (_)._ (_)._ _\<close> [100,100,100,100,100] 101)
+  | ImpR "\<guillemotleft>name\<guillemotright>(\<guillemotleft>coname\<guillemotright>trm)" "coname"       (\<open>ImpR (_).<_>._ _\<close> [100,100,100,100] 101)
+  | ImpL "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name"     (\<open>ImpL <_>._ (_)._ _\<close> [100,100,100,100,100] 101)
 
 text \<open>named terms\<close>
 
-nominal_datatype ntrm = Na "\<guillemotleft>name\<guillemotright>trm" ("((_):_)" [100,100] 100)
+nominal_datatype ntrm = Na "\<guillemotleft>name\<guillemotright>trm" (\<open>((_):_)\<close> [100,100] 100)
 
 text \<open>conamed terms\<close>
 
-nominal_datatype ctrm = Co "\<guillemotleft>coname\<guillemotright>trm" ("(<_>:_)" [100,100] 100)
+nominal_datatype ctrm = Co "\<guillemotleft>coname\<guillemotright>trm" (\<open>(<_>:_)\<close> [100,100] 100)
 
 text \<open>renaming functions\<close>
 
 nominal_primrec (freshness_context: "(d::coname,e::coname)") 
-  crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm"  ("_[_\<turnstile>c>_]" [100,0,0] 100) 
+  crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm"  (\<open>_[_\<turnstile>c>_]\<close> [100,0,0] 100) 
 where
   "(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)" 
 | "\<lbrakk>a\<sharp>(d,e,N);x\<sharp>M\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N)[d\<turnstile>c>e] = Cut <a>.(M[d\<turnstile>c>e]) (x).(N[d\<turnstile>c>e])" 
@@ -92,7 +92,7 @@
   by(finite_guess | simp add: abs_fresh abs_supp fin_supp | fresh_guess)+
 
 nominal_primrec (freshness_context: "(u::name,v::name)") 
-  nrename :: "trm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> trm"      ("_[_\<turnstile>n>_]" [100,0,0] 100) 
+  nrename :: "trm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> trm"      (\<open>_[_\<turnstile>n>_]\<close> [100,0,0] 100) 
 where
   "(Ax x a)[u\<turnstile>n>v] = (if x=u then Ax v a else Ax x a)" 
 | "\<lbrakk>a\<sharp>N;x\<sharp>(u,v,M)\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N)[u\<turnstile>n>v] = Cut <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v])" 
@@ -610,7 +610,7 @@
 qed
 
 nominal_primrec (freshness_context: "(y::name,c::coname,P::trm)")
-  substn :: "trm \<Rightarrow> name   \<Rightarrow> coname \<Rightarrow> trm \<Rightarrow> trm" ("_{_:=<_>._}" [100,100,100,100] 100) 
+  substn :: "trm \<Rightarrow> name   \<Rightarrow> coname \<Rightarrow> trm \<Rightarrow> trm" (\<open>_{_:=<_>._}\<close> [100,100,100,100] 100) 
 where
   "(Ax x a){y:=<c>.P} = (if x=y then Cut <c>.P (y).Ax y a else Ax x a)" 
 | "\<lbrakk>a\<sharp>(c,P,N);x\<sharp>(y,P,M)\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N){y:=<c>.P} = 
@@ -673,7 +673,7 @@
 done
 
 nominal_primrec (freshness_context: "(d::name,z::coname,P::trm)")
-  substc :: "trm \<Rightarrow> coname \<Rightarrow> name   \<Rightarrow> trm \<Rightarrow> trm" ("_{_:=('(_'))._}" [100,0,0,100] 100)
+  substc :: "trm \<Rightarrow> coname \<Rightarrow> name   \<Rightarrow> trm \<Rightarrow> trm" (\<open>_{_:=('(_'))._}\<close> [100,0,0,100] 100)
 where
   "(Ax x a){d:=(z).P} = (if d=a then Cut <a>.(Ax x a) (z).P else Ax x a)" 
 | "\<lbrakk>a\<sharp>(d,P,N);x\<sharp>(z,P,M)\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N){d:=(z).P} = 
@@ -2423,7 +2423,7 @@
 qed (use fic_rest_elims in force)+
 
 inductive
-  l_redu :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longrightarrow>\<^sub>l _" [100,100] 100)
+  l_redu :: "trm \<Rightarrow> trm \<Rightarrow> bool" (\<open>_ \<longrightarrow>\<^sub>l _\<close> [100,100] 100)
 where
   LAxR:  "\<lbrakk>x\<sharp>M; a\<sharp>b; fic M a\<rbrakk> \<Longrightarrow> Cut <a>.M (x).(Ax x b) \<longrightarrow>\<^sub>l M[a\<turnstile>c>b]"
 | LAxL:  "\<lbrakk>a\<sharp>M; x\<sharp>y; fin M x\<rbrakk> \<Longrightarrow> Cut <a>.(Ax y a) (x).M \<longrightarrow>\<^sub>l M[x\<turnstile>n>y]"
@@ -3044,7 +3044,7 @@
 
 
 inductive
-  c_redu :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longrightarrow>\<^sub>c _" [100,100] 100)
+  c_redu :: "trm \<Rightarrow> trm \<Rightarrow> bool" (\<open>_ \<longrightarrow>\<^sub>c _\<close> [100,100] 100)
 where
   left[intro]:  "\<lbrakk>\<not>fic M a; a\<sharp>N; x\<sharp>M\<rbrakk> \<Longrightarrow> Cut <a>.M (x).N \<longrightarrow>\<^sub>c M{a:=(x).N}"
 | right[intro]: "\<lbrakk>\<not>fin N x; a\<sharp>N; x\<sharp>M\<rbrakk> \<Longrightarrow> Cut <a>.M (x).N \<longrightarrow>\<^sub>c N{x:=<a>.M}"
@@ -3098,7 +3098,7 @@
   by (induct rule: c_redu.induct) (auto simp: abs_fresh rename_fresh subst_fresh)+
 
 inductive
-  a_redu :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longrightarrow>\<^sub>a _" [100,100] 100)
+  a_redu :: "trm \<Rightarrow> trm \<Rightarrow> bool" (\<open>_ \<longrightarrow>\<^sub>a _\<close> [100,100] 100)
 where
   al_redu[intro]: "M\<longrightarrow>\<^sub>l M' \<Longrightarrow> M \<longrightarrow>\<^sub>a M'"
 | ac_redu[intro]: "M\<longrightarrow>\<^sub>c M' \<Longrightarrow> M \<longrightarrow>\<^sub>a M'"
@@ -3477,7 +3477,7 @@
 text \<open>Transitive Closure\<close>
 
 abbreviation
- a_star_redu :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longrightarrow>\<^sub>a* _" [80,80] 80)
+ a_star_redu :: "trm \<Rightarrow> trm \<Rightarrow> bool" (\<open>_ \<longrightarrow>\<^sub>a* _\<close> [80,80] 80)
 where
   "M \<longrightarrow>\<^sub>a* M' \<equiv> (a_redu)\<^sup>*\<^sup>* M M'"