# HG changeset patch
# User kleing
# Date 1073608104 -3600
# Node ID 1fff56703e29dad1eed35a6b1167c6cb1257069e
# Parent  5b9dd0de05d0ad04188c39e1041a6c050652acb1
set isasep to {} by default

diff -r 5b9dd0de05d0 -r 1fff56703e29 lib/texinputs/isabelle.sty
--- 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=`\!