diff -r 0f0a2148a099 -r 3023d90dc59e lib/texinputs/isabelle.sty
--- 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=`\!