# HG changeset patch
# User wenzelm
# Date 997387659 -7200
# Node ID 681aa3dfab4b0ea98415fdd2faf49cb15ae7a533
# Parent  0e66e0114d9a8962e3ac6cf1c0a54bb3da6f7c0d
tuned;

diff -r 0e66e0114d9a -r 681aa3dfab4b doc-src/IsarRef/conversion.tex
--- a/doc-src/IsarRef/conversion.tex	Thu Aug 09 20:48:57 2001 +0200
+++ b/doc-src/IsarRef/conversion.tex	Thu Aug 09 22:07:39 2001 +0200
@@ -231,7 +231,7 @@
 \medskip In practice, actual rules are often rather direct consequences of
 corresponding atomic statements, typically stemming from the definition of a
 new concept.  In that case, the general scheme for deriving rules may be
-greatly simplified, using one of the standard automated proof tools, such ad
+greatly simplified, using one of the standard automated proof tools, such as
 $simp$, $blast$, or $auto$.  This would work as follows:
 \begin{matharray}{l}
   \LEMMA{}{\texttt"{\phi@1 \Imp \dots \Imp \psi}\texttt"} \\
diff -r 0e66e0114d9a -r 681aa3dfab4b doc-src/IsarRef/hol.tex
--- a/doc-src/IsarRef/hol.tex	Thu Aug 09 20:48:57 2001 +0200
+++ b/doc-src/IsarRef/hol.tex	Thu Aug 09 22:07:39 2001 +0200
@@ -92,7 +92,7 @@
 \item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]
   defines extensible record type $(\vec\alpha)t$, derived from the optional
   parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.
-  See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information only
+  See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information on
   simply-typed extensible records.
 \end{descr}