# HG changeset patch
# User haftmann
# Date 1507494499 -7200
# Node ID 128e9ed9f63c8db568a0982603646b4a0c2a8cb7
# Parent  7ba45c30250cb06024c39224da26c4196596a3e5
spelling and tuned whitespace

diff -r 7ba45c30250c -r 128e9ed9f63c src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Oct 08 22:28:19 2017 +0200
+++ b/src/HOL/Divides.thy	Sun Oct 08 22:28:19 2017 +0200
@@ -527,7 +527,7 @@
 text \<open>
   The following type class contains everything necessary to formulate
   a division algorithm in ring structures with numerals, restricted
-  to its positive segments.  This is its primary motiviation, and it
+  to its positive segments.  This is its primary motivation, and it
   could surely be formulated using a more fine-grained, more algebraic
   and less technical class hierarchy.
 \<close>
@@ -551,7 +551,6 @@
     \<comment> \<open>These are conceptually definitions but force generated code
     to be monomorphic wrt. particular instances of this class which
     yields a significant speedup.\<close>
-
 begin
 
 subclass semiring_div_parity