src/HOL/Nominal/Examples/Contexts.thy

--- a/src/HOL/Nominal/Examples/Contexts.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Nominal/Examples/Contexts.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -25,7 +25,7 @@
 nominal_datatype lam = 
     Var "name"
   | App "lam" "lam"
-  | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
+  | Lam "\<guillemotleft>name\<guillemotright>lam" (\<open>Lam [_]._\<close> [100,100] 100)
 
 text \<open>
   Contexts - the lambda case in contexts does not bind 
@@ -33,15 +33,15 @@
 \<close>
 
 nominal_datatype ctx = 
-    Hole ("\<box>" 1000)  
+    Hole (\<open>\<box>\<close> 1000)  
   | CAppL "ctx" "lam"
   | CAppR "lam" "ctx" 
-  | CLam "name" "ctx"  ("CLam [_]._" [100,100] 100) 
+  | CLam "name" "ctx"  (\<open>CLam [_]._\<close> [100,100] 100) 
 
 text \<open>Capture-Avoiding Substitution\<close>
 
 nominal_primrec
-  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)
+  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  (\<open>_[_::=_]\<close> [100,100,100] 100)
 where
   "(Var x)[y::=s] = (if x=y then s else (Var x))"
 | "(App t\<^sub>1 t\<^sub>2)[y::=s] = App (t\<^sub>1[y::=s]) (t\<^sub>2[y::=s])"
@@ -58,7 +58,7 @@
 \<close>
 
 nominal_primrec
-  filling :: "ctx \<Rightarrow> lam \<Rightarrow> lam" ("_\<lbrakk>_\<rbrakk>" [100,100] 100)
+  filling :: "ctx \<Rightarrow> lam \<Rightarrow> lam" (\<open>_\<lbrakk>_\<rbrakk>\<close> [100,100] 100)
 where
   "\<box>\<lbrakk>t\<rbrakk> = t"
 | "(CAppL E t')\<lbrakk>t\<rbrakk> = App (E\<lbrakk>t\<rbrakk>) t'"
@@ -79,7 +79,7 @@
 text \<open>The composition of two contexts.\<close>
 
 nominal_primrec
- ctx_compose :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" ("_ \<circ> _" [100,100] 100)
+ ctx_compose :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" (\<open>_ \<circ> _\<close> [100,100] 100)
 where
   "\<box> \<circ> E' = E'"
 | "(CAppL E t') \<circ> E' = CAppL (E \<circ> E') t'"
@@ -94,14 +94,14 @@
 text \<open>Beta-reduction via contexts in the Felleisen-Hieb style.\<close>
 
 inductive
-  ctx_red :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>x _" [80,80] 80) 
+  ctx_red :: "lam\<Rightarrow>lam\<Rightarrow>bool" (\<open>_ \<longrightarrow>x _\<close> [80,80] 80) 
 where
   xbeta[intro]: "E\<lbrakk>App (Lam [x].t) t'\<rbrakk> \<longrightarrow>x E\<lbrakk>t[x::=t']\<rbrakk>" 
 
 text \<open>Beta-reduction via congruence rules in the Plotkin style.\<close>
 
 inductive
-  cong_red :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>o _" [80,80] 80) 
+  cong_red :: "lam\<Rightarrow>lam\<Rightarrow>bool" (\<open>_ \<longrightarrow>o _\<close> [80,80] 80) 
 where
   obeta[intro]: "App (Lam [x].t) t' \<longrightarrow>o t[x::=t']"
 | oapp1[intro]: "t \<longrightarrow>o t' \<Longrightarrow> App t t2 \<longrightarrow>o App t' t2"