--- a/src/HOL/Proofs/Lambda/WeakNorm.thy Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy Fri Sep 20 19:51:08 2024 +0200
@@ -201,7 +201,7 @@
\<comment> \<open>A computationally relevant copy of @{term "e \<turnstile> t : T"}\<close>
-inductive rtyping :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
+inductive rtyping :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" (\<open>_ \<turnstile>\<^sub>R _ : _\<close> [50, 50, 50] 50)
where
Var: "e x = T \<Longrightarrow> e \<turnstile>\<^sub>R Var x : T"
| Abs: "e\<langle>0:T\<rangle> \<turnstile>\<^sub>R t : U \<Longrightarrow> e \<turnstile>\<^sub>R Abs t : (T \<Rightarrow> U)"