author | paulson |
Tue, 06 May 2003 10:40:43 +0200 | |
changeset 13963 | ba7aa8c426ad |
parent 13962 | 908f6776a59b |
child 13964 | bfca18e9ab72 |
--- a/doc-src/TutorialI/isabelle.sty Tue May 06 09:23:13 2003 +0200 +++ b/doc-src/TutorialI/isabelle.sty Tue May 06 10:40:43 2003 +0200 @@ -41,7 +41,7 @@ \newcommand{\isa}[1]{\emph{\isastyleminor #1}} \newcommand{\isaindent}[1]{\hphantom{#1}} -\newcommand{\isanewline}{\mbox{}\\\mbox{}} +\newcommand{\isanewline}{\mbox{}\par\mbox{}} \newcommand{\isadigit}[1]{#1} \chardef\isacharbang=`\!