# HG changeset patch
# User wenzelm
# Date 1610289148 -3600
# Node ID b4066bad7f7686379af32639f7864d41c3db94fa
# Parent  cd0cd534f9273bd12e8db71fb92174a1b19d3aaf
avoid Unicode quotes;

diff -r cd0cd534f927 -r b4066bad7f76 src/HOL/Data_Structures/Selection.thy
--- 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>