| changeset 14353 | 79f9fbef9106 |
| parent 14342 | 6e564092d72d |
| child 14732 | 967db86e853c |
--- 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=`\!