--- a/src/HOL/ex/document/root.tex Thu Sep 27 16:43:46 2001 +0200
+++ b/src/HOL/ex/document/root.tex Thu Sep 27 18:42:47 2001 +0200
@@ -9,7 +9,7 @@
\begin{document}
-\title{Miscellaneous Isabelle/HOL Examples}
+\title{Miscellaneous HOL Examples}
\maketitle
\tableofcontents