# HG changeset patch
# User nipkow
# Date 1116367999 -7200
# Node ID 251069032c031c038ac4eb1f1a96a9d0d8ca4bd4
# Parent  dd9023d84f44416c406f79ae385bf2178995e09f
documented new subst

diff -r dd9023d84f44 -r 251069032c03 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Tue May 17 19:24:15 2005 +0200
+++ b/doc-src/IsarRef/generic.tex	Wed May 18 00:13:19 2005 +0200
@@ -873,7 +873,7 @@
 \end{matharray}
 
 \begin{rail}
-  'subst' thmref
+  'subst' ('(' 'asm' ')')? ('(' (nat+) ')')? thmref
   ;
   'split' ('(' 'asm' ')')? thmrefs
   ;
@@ -887,9 +887,24 @@
 
 \begin{descr}
 
-\item [$subst~a$] performs a single substitution step using rule $a$, which
+\item [$subst~eq$] performs a single substitution step using rule $eq$, which
   may be either a meta or object equality.
 
+\item [$subst~(asm)~eq$] substitutes in an assumption.
+
+\item [$subst~(i \dots j)~eq$] performs several substitutions in the
+conclusion. The numbers $i$ to $j$ indicate the positions to substitute at.
+Positions are ordered from the top of the term tree moving down from left to
+right. For example, in $(a+b)+(c+d)$ there are three positions where
+commutativity of $+$ is applicable: 1 refers to the whole term, 2 to $a+b$
+and 3 to $c+d$. If the positions in the list $(i \dots j)$ are
+non-overlapping (e.g. $(2~3)$ in $(a+b)+(c+d)$) you may assume all
+substitutions are performed simultaneously. Otherwise the behaviour of
+$subst$ is not specified.
+
+\item [$subst~(asm)~(i \dots j)~eq$] performs the substitutions in the
+assumptions, which are treated as one big term.
+
 \item [$hypsubst$] performs substitution using some assumption; this only
   works for equations of the form $x = t$ where $x$ is a free or bound
   variable.