src/HOL/Unix/document/root.tex
changeset 11862 03801fd2f8fc
parent 11102 5ceaa79c220d
child 13381 60bc63b13857
     1.1 --- a/src/HOL/Unix/document/root.tex	Sun Oct 21 19:41:43 2001 +0200
     1.2 +++ b/src/HOL/Unix/document/root.tex	Sun Oct 21 19:42:24 2001 +0200
     1.3 @@ -6,7 +6,6 @@
     1.4  \urlstyle{rm}
     1.5  \isabellestyle{it}
     1.6  
     1.7 -\renewcommand{\isabeginpar}{\par\smallskip}
     1.8  \renewcommand{\isamarkupcmt}[1]{{\isastylecmt---~~#1}}
     1.9  
    1.10  \newcommand{\secref}[1]{\S\ref{#1}}