# HG changeset patch
# User wenzelm
# Date 1001608967 -7200
# Node ID 3df838634f2b50c633c84301d383a37dea8832fd
# Parent  4b171ad4ff6505b8e92eb62abadd92e800f0dd87
tuned;

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