added 'using' command;

--- a/doc-src/IsarRef/pure.tex	Tue Jan 03 00:06:23 2006 +0100
+++ b/doc-src/IsarRef/pure.tex	Tue Jan 03 00:06:24 2006 +0100
@@ -747,13 +747,14 @@
 \subsection{Facts and forward chaining}
 
 \indexisarcmd{note}\indexisarcmd{then}\indexisarcmd{from}\indexisarcmd{with}
-\indexisarcmd{using}
+\indexisarcmd{using}\indexisarcmd{unfolding}
 \begin{matharray}{rcl}
   \isarcmd{note} & : & \isartrans{proof(state)}{proof(state)} \\
   \isarcmd{then} & : & \isartrans{proof(state)}{proof(chain)} \\
   \isarcmd{from} & : & \isartrans{proof(state)}{proof(chain)} \\
   \isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\
   \isarcmd{using} & : & \isartrans{proof(prove)}{proof(prove)} \\
+  \isarcmd{unfolding} & : & \isartrans{proof(prove)}{proof(prove)} \\
 \end{matharray}
 
 New facts are established either by assumption or proof of local statements.
@@ -768,7 +769,7 @@
 \begin{rail}
   'note' (thmdef? thmrefs + 'and')
   ;
-  ('from' | 'with' | 'using') (thmrefs + 'and')
+  ('from' | 'with' | 'using' | 'unfolding') (thmrefs + 'and')
   ;
 \end{rail}
 
@@ -795,6 +796,10 @@
   
 \item [$\USING{\vec b}$] augments the facts being currently indicated for use
   by a subsequent refinement step (such as $\APPLYNAME$ or $\PROOFNAME$).
+  
+\item [$\UNFOLDING{\vec b}$] is structurally similar to $\USINGNAME$,
+  but unfolds meta-level equations {\vec b} throughout the goal state
+  and facts.
 
 \end{descr}
 

--- a/src/Pure/Isar/isar_syn.ML	Tue Jan 03 00:06:23 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jan 03 00:06:24 2006 +0100
@@ -398,7 +398,12 @@
 val usingP =
   OuterSyntax.command "using" "augment goal facts"
     (K.tag_proof K.prf_decl)
-    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using_thmss)));
+    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using)));
+
+val unfoldingP =
+  OuterSyntax.command "unfolding" "unfold definitions in goal and facts"
+    (K.tag_proof K.prf_decl)
+    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding)));
 
 
 (* proof context *)
@@ -854,11 +859,12 @@
   (*proof commands*)
   theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP,
   assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP,
-  withP, noteP, usingP, beginP, endP, nextP, qedP, terminal_proofP,
-  default_proofP, immediate_proofP, done_proofP, skip_proofP,
-  forget_proofP, deferP, preferP, applyP, apply_endP, proofP, alsoP,
-  finallyP, moreoverP, ultimatelyP, backP, cannot_undoP, clear_undosP,
-  redoP, undos_proofP, undoP, killP, interpretationP, interpretP,
+  withP, noteP, usingP, unfoldingP, beginP, endP, nextP, qedP,
+  terminal_proofP, default_proofP, immediate_proofP, done_proofP,
+  skip_proofP, forget_proofP, deferP, preferP, applyP, apply_endP,
+  proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
+  cannot_undoP, clear_undosP, redoP, undos_proofP, undoP, killP,
+  interpretationP, interpretP,
   (*diagnostic commands*)
   pretty_setmarginP,
   print_commandsP, print_contextP, print_theoryP, print_syntaxP,