summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Sun, 18 Aug 2013 15:35:01 +0200 | |

changeset 53070 | 6a3410845bb2 |

parent 53069 | d165213e3924 |

child 53075 | 98fc47533342 |

spelling and typos

--- a/src/HOL/Divides.thy Sun Aug 18 15:29:50 2013 +0200 +++ b/src/HOL/Divides.thy Sun Aug 18 15:35:01 2013 +0200 @@ -593,7 +593,7 @@ text {* This is a formulation of one step (referring to one digit position) in school-method division: compare the dividend at the current - digit position with the remained from previous division steps + digit position with the remainder from previous division steps and evaluate accordingly. *} @@ -2550,7 +2550,7 @@ text {* This re-embedding of natural division on integers goes back to the time when numerals had been signed numerals. It should - now be placed by the algorithm developed in @{class semiring_numeral_div}. + now be replaced by the algorithm developed in @{class semiring_numeral_div}. *} lemma div_nat_numeral [simp]: