'using' command;

--- a/etc/isar-keywords-ZF.el	Fri Feb 22 11:26:44 2002 +0100
+++ b/etc/isar-keywords-ZF.el	Sun Feb 24 21:44:43 2002 +0100
@@ -161,6 +161,7 @@
     "use"
     "use_thy"
     "use_thy_only"
+    "using"
     "welcome"
     "with"
     "{"
@@ -380,7 +381,8 @@
     "moreover"
     "note"
     "txt"
-    "txt_raw"))
+    "txt_raw"
+    "using"))
 
 (defconst isar-keywords-proof-asm
   '("assume"

--- a/etc/isar-keywords.el	Fri Feb 22 11:26:44 2002 +0100
+++ b/etc/isar-keywords.el	Sun Feb 24 21:44:43 2002 +0100
@@ -166,6 +166,7 @@
     "use"
     "use_thy"
     "use_thy_only"
+    "using"
     "welcome"
     "with"
     "{"
@@ -215,7 +216,6 @@
     "transitions"
     "transrel"
     "uses"
-    "using"
     "where"))
 
 (defconst isar-keywords-control
@@ -407,7 +407,8 @@
     "moreover"
     "note"
     "txt"
-    "txt_raw"))
+    "txt_raw"
+    "using"))
 
 (defconst isar-keywords-proof-asm
   '("assume"

--- a/src/Pure/Isar/isar_syn.ML	Fri Feb 22 11:26:44 2002 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Feb 24 21:44:43 2002 +0100
@@ -349,6 +349,10 @@
   OuterSyntax.command "note" "define facts" K.prf_decl
     (name_facts >> (Toplevel.print oo (Toplevel.proof o IsarThy.have_facts)));
 
+val usingP =
+  OuterSyntax.command "using" "augment goal facts" K.prf_decl
+    (facts >> (Toplevel.print oo (Toplevel.proof o IsarThy.using_facts)));
+
 
 (* proof context *)
 
@@ -738,11 +742,11 @@
   (*proof commands*)
   theoremP, lemmaP, corollaryP, showP, haveP, thusP, henceP, fixP,
   assumeP, presumeP, defP, obtainP, letP, caseP, thenP, fromP, withP,
-  noteP, 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,
+  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,
   (*diagnostic commands*)
   pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
   print_syntaxP, print_theoremsP, print_localesP, print_localeP,