unfold(ed): not necessrily meta equations;
authorwenzelm
Sun Apr 09 18:51:11 2006 +0200 (2006-04-09)
changeset 19379c8cf1544b5a7
parent 19378 6cc9ac729eb5
child 19380 b808efaa5828
unfold(ed): not necessrily meta equations;
doc-src/IsarRef/generic.tex
     1.1 --- a/doc-src/IsarRef/generic.tex	Sun Apr 09 14:47:24 2006 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Sun Apr 09 18:51:11 2006 +0200
     1.3 @@ -663,10 +663,11 @@
     1.4  \end{rail}
     1.5  
     1.6  \begin{descr}
     1.7 -
     1.8 -\item [$unfold~\vec a$ and $fold~\vec a$] expand (or fold back again) the
     1.9 -  given meta-level definitions throughout all goals; any chained facts
    1.10 -  provided are inserted into the goal and subject to rewriting as well.
    1.11 +  
    1.12 +\item [$unfold~\vec a$ and $fold~\vec a$] expand (or fold back again)
    1.13 +  the given definitions throughout all goals; any chained facts
    1.14 +  provided are inserted into the goal and subject to rewriting as
    1.15 +  well.
    1.16  
    1.17  \item [$insert~\vec a$] inserts theorems as facts into all goals of the proof
    1.18    state.  Note that current facts indicated for forward chaining are ignored.
    1.19 @@ -733,9 +734,9 @@
    1.20    specified); the $COMP$ version skips the automatic lifting process that is
    1.21    normally intended (cf.\ \texttt{RS} and \texttt{COMP} in
    1.22    \cite[\S5]{isabelle-ref}).
    1.23 -
    1.24 -\item [$unfolded~\vec a$ and $folded~\vec a$] expand and fold back again the
    1.25 -  given meta-level definitions throughout a rule.
    1.26 +  
    1.27 +\item [$unfolded~\vec a$ and $folded~\vec a$] expand and fold back
    1.28 +  again the given definitions throughout a rule.
    1.29  
    1.30  \item [$elim_format$] turns a destruction rule into elimination rule format,
    1.31    by resolving with the rule $\PROP A \Imp (\PROP A \Imp \PROP B) \Imp \PROP