\isaindent;
authorwenzelm
Sun Jan 21 13:21:14 2001 +0100 (2001-01-21)
changeset 1094998cdeb6beb3b
parent 10948 1bd100c82300
child 10950 aa788fcb75a5
\isaindent;
lib/texinputs/isabelle.sty
     1.1 --- a/lib/texinputs/isabelle.sty	Sat Jan 20 00:35:35 2001 +0100
     1.2 +++ b/lib/texinputs/isabelle.sty	Sun Jan 21 13:21:14 2001 +0100
     1.3 @@ -39,6 +39,7 @@
     1.4  
     1.5  \newcommand{\isa}[1]{\emph{\isastyleminor #1}}
     1.6  
     1.7 +\newcommand{\isaindent}[1]{\hphantom{#1}}
     1.8  \newcommand{\isanewline}{\mbox{}\\\mbox{}}
     1.9  \newcommand{\isadigit}[1]{#1}
    1.10