src/Pure/Isar/isar_syn.ML
changeset 12926 cd0dd6e0bf5c
parent 12876 a70df1e5bf10
child 12940 26c0566adf62
--- 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,