diff -r a8b1a44d8264 -r 79f9fbef9106 doc-src/TutorialI/isabelle.sty
--- a/doc-src/TutorialI/isabelle.sty	Mon Jan 12 16:45:35 2004 +0100
+++ b/doc-src/TutorialI/isabelle.sty	Mon Jan 12 16:51:45 2004 +0100
@@ -52,6 +52,7 @@
 
 \newcommand{\isaindent}[1]{\hphantom{#1}}
 \newcommand{\isanewline}{\mbox{}\par\mbox{}}
+\newcommand{\isasep}{} % override with e.g. \renewcommand{\isasep}{\vspace{1ex}}
 \newcommand{\isadigit}[1]{#1}
 
 \chardef\isacharbang=`\!