# HG changeset patch
# User wenzelm
# Date 1678226970 -3600
# Node ID a8fa53c086a4ccac002a7f29ef7351f5256e869d
# Parent  13b53fae16f3793f6eddbe9de8cfa278772987a7
eliminated suspicious Unicode characters;

diff -r 13b53fae16f3 -r a8fa53c086a4 src/HOL/Examples/Ackermann.thy
--- a/src/HOL/Examples/Ackermann.thy	Tue Mar 07 23:08:14 2023 +0100
+++ b/src/HOL/Examples/Ackermann.thy	Tue Mar 07 23:09:30 2023 +0100
@@ -92,7 +92,7 @@
 
 text \<open>This termination proof uses the argument from
 Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings.
-Communications of the ACM 22 (8) 1979, 465–476.\<close>
+Communications of the ACM 22 (8) 1979, 465--476.\<close>
 
 text\<open>Setting up the termination proof. Note that Dershowitz had @{term z} as a global variable.
 The top two stack elements are treated differently from the rest.\<close>