diff -r 699de91b15e2 -r d5509912af18 doc-src/TutorialI/tutorial.tex
--- a/doc-src/TutorialI/tutorial.tex	Tue Aug 29 11:52:16 2000 +0200
+++ b/doc-src/TutorialI/tutorial.tex	Tue Aug 29 11:52:47 2000 +0200
@@ -22,9 +22,7 @@
 \newcommand{\isasymFun}{\isasymRightarrow}
 \newcommand{\isasymuniqex}{\emph{$\exists!\,$}}
 
-\newenvironment{isabellepar}%
-{\par\medskip\noindent\begin{isabelle}}{\end{isabelle}\medskip\par\noindent}
-
+\newenvironment{isabellepar}{\medskip\begin{isabelle}}{\end{isabelle}\medskip}
 \renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}}
 
 %%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}