| changeset 10950 | aa788fcb75a5 |
| parent 10839 | 1f93f5a27de6 |
| child 11610 | 99103cef5f29 |
--- 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}