# HG changeset patch
# User nipkow
# Date 1116518825 -7200
# Node ID 0705c8d1f107433c8eac147b4fed5e9f18af29b8
# Parent  a6d480e6c5f06281b58e96e3797555a34b1ce1d9
subst again

diff -r a6d480e6c5f0 -r 0705c8d1f107 doc-src/IsarRef/generic.tex
--- 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