# HG changeset patch
# User wenzelm
# Date 1144601471 -7200
# Node ID c8cf1544b5a7b86703e3f1302316fb1f1c2e3057
# Parent  6cc9ac729eb55ae55c011a16a892c251dbc1e64d
unfold(ed): not necessrily meta equations;

diff -r 6cc9ac729eb5 -r c8cf1544b5a7 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Sun Apr 09 14:47:24 2006 +0200
+++ b/doc-src/IsarRef/generic.tex	Sun Apr 09 18:51:11 2006 +0200
@@ -663,10 +663,11 @@
 \end{rail}
 
 \begin{descr}
-
-\item [$unfold~\vec a$ and $fold~\vec a$] expand (or fold back again) the
-  given meta-level definitions throughout all goals; any chained facts
-  provided are inserted into the goal and subject to rewriting as well.
+  
+\item [$unfold~\vec a$ and $fold~\vec a$] expand (or fold back again)
+  the given definitions throughout all goals; any chained facts
+  provided are inserted into the goal and subject to rewriting as
+  well.
 
 \item [$insert~\vec a$] inserts theorems as facts into all goals of the proof
   state.  Note that current facts indicated for forward chaining are ignored.
@@ -733,9 +734,9 @@
   specified); the $COMP$ version skips the automatic lifting process that is
   normally intended (cf.\ \texttt{RS} and \texttt{COMP} in
   \cite[\S5]{isabelle-ref}).
-
-\item [$unfolded~\vec a$ and $folded~\vec a$] expand and fold back again the
-  given meta-level definitions throughout a rule.
+  
+\item [$unfolded~\vec a$ and $folded~\vec a$] expand and fold back
+  again the given definitions throughout a rule.
 
 \item [$elim_format$] turns a destruction rule into elimination rule format,
   by resolving with the rule $\PROP A \Imp (\PROP A \Imp \PROP B) \Imp \PROP