# HG changeset patch
# User wenzelm
# Date 1152019829 -7200
# Node ID 5e829405e1a8949e06ab3a503dc7d62b878080a1
# Parent  05f940b9ef15e160db363be21528b600fa3b657d
tuned;

diff -r 05f940b9ef15 -r 5e829405e1a8 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Tue Jul 04 15:30:28 2006 +0200
+++ b/doc-src/IsarRef/pure.tex	Tue Jul 04 15:30:29 2006 +0200
@@ -839,12 +839,13 @@
 \item [$\WITH{\vec b}$] abbreviates ``$\FROM{\vec b~\AND~this}$''; thus the
   forward chaining is from earlier facts together with the current ones.
   
-\item [$\USING{\vec b}$] augments the facts being currently indicated for use
-  by a subsequent refinement step (such as $\APPLYNAME$ or $\PROOFNAME$).
+\item [$\USING{\vec b}$] augments the facts being currently indicated
+  for use by a subsequent refinement step (such as $\APPLYNAME$ or
+  $\PROOFNAME$).
   
-\item [$\isarcmd{unfolding}~\vec b$] is structurally similar to
-  $\USINGNAME$, but unfolds meta-level equations $\vec b$ throughout
-  the goal state and facts.
+\item [$\UNFOLDING{\vec b}$] is structurally similar to $\USINGNAME$,
+  but unfolds definitional equations $\vec b$ throughout the goal
+  state and facts.
 
 \end{descr}