--- a/doc-src/HOL/HOL.tex Thu Sep 21 14:55:46 2000 +0200
+++ b/doc-src/HOL/HOL.tex Thu Sep 21 15:58:13 2000 +0200
@@ -1767,7 +1767,7 @@
characteristic properties (see {\S}\ref{sec:HOL:record-thms}).
There is an example theory demonstrating most basic aspects of extensible
-records (see theory \texttt{HOL/ex/Points} in the Isabelle sources).
+records (see theory \texttt{HOL/ex/Records} in the Isabelle sources).
\subsection{Defining records}\label{sec:HOL:record-def}
@@ -1937,7 +1937,7 @@
\medskip
-The example theory \texttt{HOL/ex/Points} demonstrates typical proofs
+The example theory \texttt{HOL/ex/Records} demonstrates typical proofs
concerning records. The basic idea is to make \ttindex{record_split_tac}
expand quantified record variables and then simplify by the conversion rules.
By using a combination of the simplifier and classical prover together with