diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Nominal/Examples/Pattern.thy
--- a/src/HOL/Nominal/Examples/Pattern.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Nominal/Examples/Pattern.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -5,14 +5,14 @@
 begin
 
 no_syntax
-  "_Map" :: "maplets => 'a \<rightharpoonup> 'b"  ("(1[_])")
+  "_Map" :: "maplets => 'a \<rightharpoonup> 'b"  (\<open>(1[_])\<close>)
 
 atom_decl name
 
 nominal_datatype ty =
     Atom nat
-  | Arrow ty ty  (infixr "\<rightarrow>" 200)
-  | TupleT ty ty  (infixr "\<otimes>" 210)
+  | Arrow ty ty  (infixr \<open>\<rightarrow>\<close> 200)
+  | TupleT ty ty  (infixr \<open>\<otimes>\<close> 210)
 
 lemma fresh_type [simp]: "(a::name) \<sharp> (T::ty)"
   by (induct T rule: ty.induct) (simp_all add: fresh_nat)
@@ -25,22 +25,22 @@
 
 nominal_datatype trm =
     Var name
-  | Tuple trm trm  ("(1'\<langle>_,/ _'\<rangle>)")
+  | Tuple trm trm  (\<open>(1'\<langle>_,/ _'\<rangle>)\<close>)
   | Abs ty "\<guillemotleft>name\<guillemotright>trm"
-  | App trm trm  (infixl "\<cdot>" 200)
+  | App trm trm  (infixl \<open>\<cdot>\<close> 200)
   | Let ty trm btrm
 and btrm =
     Base trm
   | Bind ty "\<guillemotleft>name\<guillemotright>btrm"
 
 abbreviation
-  Abs_syn :: "name \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm"  ("(3\<lambda>_:_./ _)" [0, 0, 10] 10) 
+  Abs_syn :: "name \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm"  (\<open>(3\<lambda>_:_./ _)\<close> [0, 0, 10] 10) 
 where
   "\<lambda>x:T. t \<equiv> Abs T x t"
 
 datatype pat =
     PVar name ty
-  | PTuple pat pat  ("(1'\<langle>\<langle>_,/ _'\<rangle>\<rangle>)")
+  | PTuple pat pat  (\<open>(1'\<langle>\<langle>_,/ _'\<rangle>\<rangle>)\<close>)
 
 (* FIXME: The following should be done automatically by the nominal package *)
 overloading pat_perm \<equiv> "perm :: name prm \<Rightarrow> pat \<Rightarrow> pat" (unchecked)
@@ -83,7 +83,7 @@
 
 (* the following function cannot be defined using nominal_primrec, *)
 (* since variable parameters are currently not allowed.            *)
-primrec abs_pat :: "pat \<Rightarrow> btrm \<Rightarrow> btrm" ("(3\<lambda>[_]./ _)" [0, 10] 10)
+primrec abs_pat :: "pat \<Rightarrow> btrm \<Rightarrow> btrm" (\<open>(3\<lambda>[_]./ _)\<close> [0, 10] 10)
 where
   "(\<lambda>[PVar x T]. t) = Bind T x t"
 | "(\<lambda>[\<langle>\<langle>p, q\<rangle>\<rangle>]. t) = (\<lambda>[p]. \<lambda>[q]. t)"
@@ -143,7 +143,7 @@
 type_synonym ctx = "(name \<times> ty) list"
 
 inductive
-  ptyping :: "pat \<Rightarrow> ty \<Rightarrow> ctx \<Rightarrow> bool"  ("\<turnstile> _ : _ \<Rightarrow> _" [60, 60, 60] 60)
+  ptyping :: "pat \<Rightarrow> ty \<Rightarrow> ctx \<Rightarrow> bool"  (\<open>\<turnstile> _ : _ \<Rightarrow> _\<close> [60, 60, 60] 60)
 where
   PVar: "\<turnstile> PVar x T : T \<Rightarrow> [(x, T)]"
 | PTuple: "\<turnstile> p : T \<Rightarrow> \<Delta>\<^sub>1 \<Longrightarrow> \<turnstile> q : U \<Rightarrow> \<Delta>\<^sub>2 \<Longrightarrow> \<turnstile> \<langle>\<langle>p, q\<rangle>\<rangle> : T \<otimes> U \<Rightarrow> \<Delta>\<^sub>2 @ \<Delta>\<^sub>1"
@@ -168,16 +168,16 @@
   by (induct \<Gamma>) (auto simp add: fresh_ctxt_set_eq [symmetric])
 
 abbreviation
-  "sub_ctx" :: "ctx \<Rightarrow> ctx \<Rightarrow> bool" ("_ \<sqsubseteq> _") 
+  "sub_ctx" :: "ctx \<Rightarrow> ctx \<Rightarrow> bool" (\<open>_ \<sqsubseteq> _\<close>) 
 where
   "\<Gamma>\<^sub>1 \<sqsubseteq> \<Gamma>\<^sub>2 \<equiv> \<forall>x. x \<in> set \<Gamma>\<^sub>1 \<longrightarrow> x \<in> set \<Gamma>\<^sub>2"
 
 abbreviation
-  Let_syn :: "pat \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm"  ("(LET (_ =/ _)/ IN (_))" 10)
+  Let_syn :: "pat \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm"  (\<open>(LET (_ =/ _)/ IN (_))\<close> 10)
 where
   "LET p = t IN u \<equiv> Let (pat_type p) t (\<lambda>[p]. Base u)"
 
-inductive typing :: "ctx \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60, 60, 60] 60)
+inductive typing :: "ctx \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool" (\<open>_ \<turnstile> _ : _\<close> [60, 60, 60] 60)
 where
   Var [intro]: "valid \<Gamma> \<Longrightarrow> (x, T) \<in> set \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
 | Tuple [intro]: "\<Gamma> \<turnstile> t : T \<Longrightarrow> \<Gamma> \<turnstile> u : U \<Longrightarrow> \<Gamma> \<turnstile> \<langle>t, u\<rangle> : T \<otimes> U"
@@ -268,7 +268,7 @@
 qed auto
 
 inductive
-  match :: "pat \<Rightarrow> trm \<Rightarrow> (name \<times> trm) list \<Rightarrow> bool"  ("\<turnstile> _ \<rhd> _ \<Rightarrow> _" [50, 50, 50] 50)
+  match :: "pat \<Rightarrow> trm \<Rightarrow> (name \<times> trm) list \<Rightarrow> bool"  (\<open>\<turnstile> _ \<rhd> _ \<Rightarrow> _\<close> [50, 50, 50] 50)
 where
   PVar: "\<turnstile> PVar x T \<rhd> t \<Rightarrow> [(x, t)]"
 | PProd: "\<turnstile> p \<rhd> t \<Rightarrow> \<theta> \<Longrightarrow> \<turnstile> q \<rhd> u \<Rightarrow> \<theta>' \<Longrightarrow> \<turnstile> \<langle>\<langle>p, q\<rangle>\<rangle> \<rhd> \<langle>t, u\<rangle> \<Rightarrow> \<theta> @ \<theta>'"
@@ -287,8 +287,8 @@
   by (induct \<theta>) (auto simp add: eqvts)
  
 nominal_primrec
-  psubst :: "(name \<times> trm) list \<Rightarrow> trm \<Rightarrow> trm"  ("_\<lparr>_\<rparr>" [95,0] 210)
-  and psubstb :: "(name \<times> trm) list \<Rightarrow> btrm \<Rightarrow> btrm"  ("_\<lparr>_\<rparr>\<^sub>b" [95,0] 210)
+  psubst :: "(name \<times> trm) list \<Rightarrow> trm \<Rightarrow> trm"  (\<open>_\<lparr>_\<rparr>\<close> [95,0] 210)
+  and psubstb :: "(name \<times> trm) list \<Rightarrow> btrm \<Rightarrow> btrm"  (\<open>_\<lparr>_\<rparr>\<^sub>b\<close> [95,0] 210)
 where
   "\<theta>\<lparr>Var x\<rparr> = (lookup \<theta> x)"
 | "\<theta>\<lparr>t \<cdot> u\<rparr> = \<theta>\<lparr>t\<rparr> \<cdot> \<theta>\<lparr>u\<rparr>"
@@ -320,12 +320,12 @@
     (simp_all add: eqvts fresh_bij)
 
 abbreviation 
-  subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_[_\<mapsto>_]" [100,0,0] 100)
+  subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" (\<open>_[_\<mapsto>_]\<close> [100,0,0] 100)
 where 
   "t[x\<mapsto>t'] \<equiv> [(x,t')]\<lparr>t\<rparr>"
 
 abbreviation 
-  substb :: "btrm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> btrm" ("_[_\<mapsto>_]\<^sub>b" [100,0,0] 100)
+  substb :: "btrm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> btrm" (\<open>_[_\<mapsto>_]\<^sub>b\<close> [100,0,0] 100)
 where 
   "t[x\<mapsto>t']\<^sub>b \<equiv> [(x,t')]\<lparr>t\<rparr>\<^sub>b"
 
@@ -525,7 +525,7 @@
 
 lemmas match_type = match_type_aux [where \<Gamma>\<^sub>1="[]", simplified]
 
-inductive eval :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longmapsto> _" [60,60] 60)
+inductive eval :: "trm \<Rightarrow> trm \<Rightarrow> bool" (\<open>_ \<longmapsto> _\<close> [60,60] 60)
 where
   TupleL: "t \<longmapsto> t' \<Longrightarrow> \<langle>t, u\<rangle> \<longmapsto> \<langle>t', u\<rangle>"
 | TupleR: "u \<longmapsto> u' \<Longrightarrow> \<langle>t, u\<rangle> \<longmapsto> \<langle>t, u'\<rangle>"