--- a/doc-src/IsarRef/generic.tex Thu May 19 11:08:15 2005 +0200
+++ b/doc-src/IsarRef/generic.tex Thu May 19 18:07:05 2005 +0200
@@ -903,7 +903,8 @@
$subst$ is not specified.
\item [$subst~(asm)~(i \dots j)~eq$] performs the substitutions in the
-assumptions, which are treated as one big term.
+assumptions. Positions $1 \dots i@1$ refer
+to assumption 1, positions $i@1+1 \dots i@2$ to assumption 2, and so on.
\item [$hypsubst$] performs substitution using some assumption; this only
works for equations of the form $x = t$ where $x$ is a free or bound