| changeset 14347 | 1fff56703e29 |
| parent 14345 | 3023d90dc59e |
| child 14708 | c0a65132d79a |
--- a/lib/texinputs/isabelle.sty Thu Jan 08 16:35:46 2004 +0100 +++ b/lib/texinputs/isabelle.sty Fri Jan 09 01:28:24 2004 +0100 @@ -52,7 +52,7 @@ \newcommand{\isaindent}[1]{\hphantom{#1}} \newcommand{\isanewline}{\mbox{}\par\mbox{}} -\newcommand{\isasep}{\vspace*{2cm}} +\newcommand{\isasep}{} % override with e.g. \renewcommand{\isasep}{\vspace{1ex}} \newcommand{\isadigit}[1]{#1} \chardef\isacharbang=`\!