--- 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