doc-src/IsarRef/generic.tex
changeset 8195 af2575a5c5ae
parent 7990 0a604b2fc2b1
child 8203 2fcc6017cb72
     1.1 --- a/doc-src/IsarRef/generic.tex	Fri Feb 04 21:53:36 2000 +0100
     1.2 +++ b/doc-src/IsarRef/generic.tex	Sat Feb 05 16:54:27 2000 +0100
     1.3 @@ -3,12 +3,14 @@
     1.4  
     1.5  \section{Basic proof methods}\label{sec:pure-meth}
     1.6  
     1.7 -\indexisarmeth{fail}\indexisarmeth{succeed}\indexisarmeth{$-$}\indexisarmeth{assumption}
     1.8 +\indexisarmeth{fail}\indexisarmeth{succeed}\indexisarmeth{$-$}
     1.9 +\indexisarmeth{assumption}\indexisarmeth{this}
    1.10  \indexisarmeth{fold}\indexisarmeth{unfold}
    1.11  \indexisarmeth{rule}\indexisarmeth{erule}
    1.12  \begin{matharray}{rcl}
    1.13    - & : & \isarmeth \\
    1.14    assumption & : & \isarmeth \\
    1.15 +  this & : & \isarmeth \\
    1.16    rule & : & \isarmeth \\
    1.17    erule^* & : & \isarmeth \\[0.5ex]
    1.18    fold & : & \isarmeth \\
    1.19 @@ -29,8 +31,9 @@
    1.20    plain \emph{do-nothing} proof step would be $\PROOF{-}$ rather than
    1.21    $\PROOFNAME$ alone.
    1.22  \item [$assumption$] solves some goal by assumption.  Any facts given are
    1.23 -  guaranteed to participate in the refinement.  Note that ``$\DOT$'' (dot)
    1.24 -  abbreviates $\BY{assumption}$.
    1.25 +  guaranteed to participate in the refinement.
    1.26 +\item [$this$] applies the current facts directly as rules.  Note that
    1.27 +  ``$\DOT$'' (dot) abbreviates $\BY{this}$.
    1.28  \item [$rule~thms$] applies some rule given as argument in backward manner;
    1.29    facts are used to reduce the rule before applying it to the goal.  Thus
    1.30    $rule$ without facts is plain \emph{introduction}, while with facts it