set isasep to {} by default
authorkleing
Fri Jan 09 01:28:24 2004 +0100 (2004-01-09)
changeset 143471fff56703e29
parent 14346 5b9dd0de05d0
child 14348 744c868ee0b7
set isasep to {} by default
lib/texinputs/isabelle.sty
     1.1 --- a/lib/texinputs/isabelle.sty	Thu Jan 08 16:35:46 2004 +0100
     1.2 +++ b/lib/texinputs/isabelle.sty	Fri Jan 09 01:28:24 2004 +0100
     1.3 @@ -52,7 +52,7 @@
     1.4  
     1.5  \newcommand{\isaindent}[1]{\hphantom{#1}}
     1.6  \newcommand{\isanewline}{\mbox{}\par\mbox{}}
     1.7 -\newcommand{\isasep}{\vspace*{2cm}}
     1.8 +\newcommand{\isasep}{} % override with e.g. \renewcommand{\isasep}{\vspace{1ex}}
     1.9  \newcommand{\isadigit}[1]{#1}
    1.10  
    1.11  \chardef\isacharbang=`\!