# HG changeset patch
# User haftmann
# Date 1376832901 -7200
# Node ID 6a3410845bb26b9f88b2ead447f912858df9bfe2
# Parent  d165213e3924c07c80294de465707748d829bbd0
spelling and typos

diff -r d165213e3924 -r 6a3410845bb2 src/HOL/Divides.thy
--- 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]: