# HG changeset patch
# User wenzelm
# Date 1442694746 -7200
# Node ID 94efa2688ff6b8c9b52df0e61f02f6dd5011957a
# Parent  a5674da43c2bb9c47bad61711916326febe79463
eliminated suspicious unicode;

diff -r a5674da43c2b -r 94efa2688ff6 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sat Sep 19 22:32:13 2015 +0200
+++ b/src/HOL/Divides.thy	Sat Sep 19 22:32:26 2015 +0200
@@ -733,7 +733,7 @@
   with False show ?thesis by simp
 qed
 
-text \<open>The division rewrite proper – first, trivial results involving @{text 1}\<close>
+text \<open>The division rewrite proper -- first, trivial results involving @{text 1}\<close>
 
 lemma divmod_trivial [simp, code]:
   "divmod Num.One Num.One = (numeral Num.One, 0)"