--- a/src/HOL/CTL/document/root.tex Sun Oct 21 19:41:43 2001 +0200
+++ b/src/HOL/CTL/document/root.tex Sun Oct 21 19:42:24 2001 +0200
@@ -23,7 +23,6 @@
\bigskip
\parindent 0pt\parskip 0.5ex
-\newcommand{\tweakskip}{\vspace{-\smallskipamount}\vspace{-\parskip}}
\input{session}