--- 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,