src/HOL/Divides.thy
changeset 53070 6a3410845bb2
parent 53069 d165213e3924
child 53199 7a9fe70c8b0a
     1.1 --- a/src/HOL/Divides.thy	Sun Aug 18 15:29:50 2013 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sun Aug 18 15:35:01 2013 +0200
     1.3 @@ -593,7 +593,7 @@
     1.4  text {*
     1.5    This is a formulation of one step (referring to one digit position)
     1.6    in school-method division: compare the dividend at the current
     1.7 -  digit position with the remained from previous division steps
     1.8 +  digit position with the remainder from previous division steps
     1.9    and evaluate accordingly.
    1.10  *}
    1.11  
    1.12 @@ -2550,7 +2550,7 @@
    1.13  text {*
    1.14    This re-embedding of natural division on integers goes back to the
    1.15    time when numerals had been signed numerals.  It should
    1.16 -  now be placed by the algorithm developed in @{class semiring_numeral_div}.  
    1.17 +  now be replaced by the algorithm developed in @{class semiring_numeral_div}.  
    1.18  *}
    1.19  
    1.20  lemma div_nat_numeral [simp]: