\isaindent;
authorwenzelm
Sun, 21 Jan 2001 13:21:14 +0100
changeset 10949 98cdeb6beb3b
parent 10948 1bd100c82300
child 10950 aa788fcb75a5
\isaindent;
lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Sat Jan 20 00:35:35 2001 +0100
+++ b/lib/texinputs/isabelle.sty	Sun Jan 21 13:21:14 2001 +0100
@@ -39,6 +39,7 @@
 
 \newcommand{\isa}[1]{\emph{\isastyleminor #1}}
 
+\newcommand{\isaindent}[1]{\hphantom{#1}}
 \newcommand{\isanewline}{\mbox{}\\\mbox{}}
 \newcommand{\isadigit}[1]{#1}