--- a/src/HOL/Hahn_Banach/document/root.tex Mon Oct 19 17:19:53 2015 +0200
+++ b/src/HOL/Hahn_Banach/document/root.tex Mon Oct 19 17:45:36 2015 +0200
@@ -8,7 +8,6 @@
\urlstyle{rm}
\newcommand{\isasymsup}{\isamath{\sup\,}}
-\newcommand{\skp}{\smallskip}
\begin{document}