diff -r a5f86aed785b -r a977245dfc8a doc-src/TutorialI/tutorial.tex
--- a/doc-src/TutorialI/tutorial.tex	Tue Aug 29 15:43:29 2000 +0200
+++ b/doc-src/TutorialI/tutorial.tex	Tue Aug 29 16:05:13 2000 +0200
@@ -4,8 +4,6 @@
 \usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment}
 \usepackage{../pdfsetup}    %last package!
 
-\newcommand\Out[1]{\texttt{\textsl{#1}}}   %% for output from terminal sessions
-
 %\newtheorem{theorem}{Theorem}[section]
 \newtheorem{Exercise}{Exercise}[section]
 \newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}
@@ -22,7 +20,6 @@
 \newcommand{\isasymFun}{\isasymRightarrow}
 \newcommand{\isasymuniqex}{\emph{$\exists!\,$}}
 
-\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}