documented new subst
authornipkow
Wed May 18 00:13:19 2005 +0200 (2005-05-18)
changeset 15995251069032c03
parent 15994 dd9023d84f44
child 15996 3699351b8939
documented new subst
doc-src/IsarRef/generic.tex
     1.1 --- a/doc-src/IsarRef/generic.tex	Tue May 17 19:24:15 2005 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Wed May 18 00:13:19 2005 +0200
     1.3 @@ -873,7 +873,7 @@
     1.4  \end{matharray}
     1.5  
     1.6  \begin{rail}
     1.7 -  'subst' thmref
     1.8 +  'subst' ('(' 'asm' ')')? ('(' (nat+) ')')? thmref
     1.9    ;
    1.10    'split' ('(' 'asm' ')')? thmrefs
    1.11    ;
    1.12 @@ -887,9 +887,24 @@
    1.13  
    1.14  \begin{descr}
    1.15  
    1.16 -\item [$subst~a$] performs a single substitution step using rule $a$, which
    1.17 +\item [$subst~eq$] performs a single substitution step using rule $eq$, which
    1.18    may be either a meta or object equality.
    1.19  
    1.20 +\item [$subst~(asm)~eq$] substitutes in an assumption.
    1.21 +
    1.22 +\item [$subst~(i \dots j)~eq$] performs several substitutions in the
    1.23 +conclusion. The numbers $i$ to $j$ indicate the positions to substitute at.
    1.24 +Positions are ordered from the top of the term tree moving down from left to
    1.25 +right. For example, in $(a+b)+(c+d)$ there are three positions where
    1.26 +commutativity of $+$ is applicable: 1 refers to the whole term, 2 to $a+b$
    1.27 +and 3 to $c+d$. If the positions in the list $(i \dots j)$ are
    1.28 +non-overlapping (e.g. $(2~3)$ in $(a+b)+(c+d)$) you may assume all
    1.29 +substitutions are performed simultaneously. Otherwise the behaviour of
    1.30 +$subst$ is not specified.
    1.31 +
    1.32 +\item [$subst~(asm)~(i \dots j)~eq$] performs the substitutions in the
    1.33 +assumptions, which are treated as one big term.
    1.34 +
    1.35  \item [$hypsubst$] performs substitution using some assumption; this only
    1.36    works for equations of the form $x = t$ where $x$ is a free or bound
    1.37    variable.