# 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 \ - The option ‘domintros’ here allows us to explicitly reason about where the function does and + The option \domintros\ 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>\mom_select\. \