src/HOL/BNF_Def.thy

--- a/src/HOL/BNF_Def.thy	Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/BNF_Def.thy	Mon Sep 23 13:32:38 2024 +0200
@@ -84,7 +84,7 @@
 lemma collect_comp: "collect F \<circ> g = collect ((\<lambda>f. f \<circ> g) ` F)"
   by (rule ext) (simp add: collect_def)
 
-definition convol ("\<langle>(_,/ _)\<rangle>") where
+definition convol (\<open>\<langle>(_,/ _)\<rangle>\<close>) where
   "\<langle>f, g\<rangle> \<equiv> \<lambda>a. (f a, g a)"
 
 lemma fst_convol: "fst \<circ> \<langle>f, g\<rangle> = f"