| changeset 14345 | 3023d90dc59e |
| parent 14332 | fd3535af90ab |
| child 14347 | 1fff56703e29 |
--- a/lib/texinputs/isabelle.sty Thu Jan 08 04:32:52 2004 +0100 +++ b/lib/texinputs/isabelle.sty Thu Jan 08 08:14:00 2004 +0100 @@ -52,6 +52,7 @@ \newcommand{\isaindent}[1]{\hphantom{#1}} \newcommand{\isanewline}{\mbox{}\par\mbox{}} +\newcommand{\isasep}{\vspace*{2cm}} \newcommand{\isadigit}[1]{#1} \chardef\isacharbang=`\!