doc-src/TutorialI/Types/numerics.tex

 \rulename{DIVISION_BY_ZERO_MOD}
 \end{isabelle}
 As a concession to convention, these equations are not installed as default
 simplification rules but are merely used to remove nonzero-divisor
 hypotheses by case analysis.  In \isa{div_mult_mult1} above, one of
-the two divisors (namely~\isa{c}) must be still be nonzero.
+the two divisors (namely~\isa{c}) must still be nonzero.
 
 The \textbf{divides} relation has the standard definition, which
 is overloaded over all numeric types: 
 \begin{isabelle}
 m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k