spelling and tuned whitespace
authorhaftmann
Sun Oct 08 22:28:19 2017 +0200 (19 months ago)
changeset 66800128e9ed9f63c
parent 66799 7ba45c30250c
child 66801 f3fda9777f9a
spelling and tuned whitespace
src/HOL/Divides.thy
     1.1 --- a/src/HOL/Divides.thy	Sun Oct 08 22:28:19 2017 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sun Oct 08 22:28:19 2017 +0200
     1.3 @@ -527,7 +527,7 @@
     1.4  text \<open>
     1.5    The following type class contains everything necessary to formulate
     1.6    a division algorithm in ring structures with numerals, restricted
     1.7 -  to its positive segments.  This is its primary motiviation, and it
     1.8 +  to its positive segments.  This is its primary motivation, and it
     1.9    could surely be formulated using a more fine-grained, more algebraic
    1.10    and less technical class hierarchy.
    1.11  \<close>
    1.12 @@ -551,7 +551,6 @@
    1.13      \<comment> \<open>These are conceptually definitions but force generated code
    1.14      to be monomorphic wrt. particular instances of this class which
    1.15      yields a significant speedup.\<close>
    1.16 -
    1.17  begin
    1.18  
    1.19  subclass semiring_div_parity