author | kleing |
Mon, 28 Apr 2003 17:52:52 +0200 | |
changeset 13933 | b224c2fd4288 |
parent 13932 | 0eb3d91b519a |
child 13934 | 8c23dea4648e |
--- a/lib/texinputs/isabelle.sty Mon Apr 28 12:01:45 2003 +0200 +++ b/lib/texinputs/isabelle.sty Mon Apr 28 17:52:52 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=`\!