set isasep to {} by default
authorkleing
Fri, 09 Jan 2004 01:28:24 +0100
changeset 14347 1fff56703e29
parent 14346 5b9dd0de05d0
child 14348 744c868ee0b7
set isasep to {} by default
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=`\!