| changeset 10950 | aa788fcb75a5 |
| parent 10861 | f2ffa2d97533 |
| child 11964 | 828ea309dc21 |
--- a/doc-src/AxClass/generated/isabelle.sty Sun Jan 21 13:21:14 2001 +0100 +++ b/doc-src/AxClass/generated/isabelle.sty Sun Jan 21 19:50:43 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}