summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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