# HG changeset patch # User wenzelm # Date 980079674 -3600 # Node ID 98cdeb6beb3b0580842a39e9a63f64aca74e6282 # Parent 1bd100c8230069af1f88e7029aa9b7dc1d751f84 \isaindent; diff -r 1bd100c82300 -r 98cdeb6beb3b 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}