
diff -r 98cdeb6beb3b -r aa788fcb75a5 doc-src/TutorialI/isabelle.sty
--- a/doc-src/TutorialI/isabelle.sty	Sun Jan 21 13:21:14 2001 +0100
+++ b/doc-src/TutorialI/isabelle.sty	Sun Jan 21 19:50:43 2001 +0100
@@ -39,6 +39,7 @@
 
 \newcommand{\isa}[1]{\emph{\isastyleminor #1}}
 
+\newcommand{\isaindent}[1]{\hphantom{#1}}
 \newcommand{\isanewline}{\mbox{}\\\mbox{}}
 \newcommand{\isadigit}[1]{#1}
 




