diff -r 4b171ad4ff65 -r 3df838634f2b src/HOL/ex/document/root.tex
--- 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