| changeset 10949 | 98cdeb6beb3b |
| parent 10822 | d72dac8e6ef5 |
| child 11573 | 4f85af77038f |
--- 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}