# 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}