
diff -r 38d8075ebff6 -r 03801fd2f8fc src/HOL/Unix/document/root.tex
--- a/src/HOL/Unix/document/root.tex	Sun Oct 21 19:41:43 2001 +0200
+++ b/src/HOL/Unix/document/root.tex	Sun Oct 21 19:42:24 2001 +0200
@@ -6,7 +6,6 @@
 \urlstyle{rm}
 \isabellestyle{it}
 
-\renewcommand{\isabeginpar}{\par\smallskip}
 \renewcommand{\isamarkupcmt}[1]{{\isastylecmt---~~#1}}
 
 \newcommand{\secref}[1]{\S\ref{#1}}




