author nipkow Thu, 19 May 2005 18:07:05 +0200 changeset 16010 0705c8d1f107 parent 16009 a6d480e6c5f0 child 16011 237aafbdb1f4
subst again
--- 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