# HG changeset patch
# User wenzelm
# Date 1434807816 -7200
# Node ID 24c2ef12318b9f2672adf56aed4387359101feba
# Parent  190b4a7d8b87e76d0d0c24578c3a6878a090bc3b
avoid suspicious Unicode;

diff -r 190b4a7d8b87 -r 24c2ef12318b src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Fri Jun 19 23:51:30 2015 +0200
+++ b/src/HOL/Rings.thy	Sat Jun 20 15:43:36 2015 +0200
@@ -811,7 +811,8 @@
 qed
   
 
-text \<open>Associated elements in a ring – an equivalence relation induced by the quasi-order divisibility \<close>
+text \<open>Associated elements in a ring --- an equivalence relation induced
+  by the quasi-order divisibility.\<close>
 
 definition associated :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
 where