author | wenzelm |
Sat, 20 Jun 2015 15:43:36 +0200 | |
changeset 60529 | 24c2ef12318b |
parent 60528 | 190b4a7d8b87 |
child 60530 | 44f9873d6f6f |
src/HOL/Rings.thy | file | annotate | diff | comparison | revisions |
--- 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