--- 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"} \\
--- 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}