--- a/src/HOL/Data_Structures/Selection.thy Sun Jan 10 15:14:27 2021 +0100
+++ b/src/HOL/Data_Structures/Selection.thy Sun Jan 10 15:32:28 2021 +0100
@@ -673,7 +673,7 @@
by (induction d xs rule: T_chop.induct) (auto simp: T_chop_reduce T_take_eq T_drop_eq)
text \<open>
- The option ‘domintros’ here allows us to explicitly reason about where the function does and
+ The option \<open>domintros\<close> here allows us to explicitly reason about where the function does and
does not terminate. With this, we can skip the termination proof this time because we can
reuse the one for \<^const>\<open>mom_select\<close>.
\<close>