src/Pure/Isar/isar_syn.ML
changeset 6878 1e97e7fbcca5
parent 6869 850812ed9976
child 6886 7d0f7ad5a35f
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Jul 01 21:25:58 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Jul 01 21:27:04 1999 +0200
     1.3 @@ -280,6 +280,10 @@
     1.4    OuterSyntax.command "from" "forward chaining from given facts" K.prf_chain
     1.5      (P.xthms1 -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.from_facts)));
     1.6  
     1.7 +val withP =
     1.8 +  OuterSyntax.command "with" "forward chaining from given and current facts" K.prf_chain
     1.9 +    (P.xthms1 -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.with_facts)));
    1.10 +
    1.11  val noteP =
    1.12    OuterSyntax.command "note" "define facts" K.prf_decl
    1.13      (facts -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.have_facts)));
    1.14 @@ -366,13 +370,16 @@
    1.15  
    1.16  (* calculational proof commands *)
    1.17  
    1.18 +val calc_args =
    1.19 +  Scan.option (P.$$$ "(" |-- P.!!! ((P.xthms1 --| P.$$$ ")") -- P.interest));
    1.20 +
    1.21  val alsoP =
    1.22    OuterSyntax.command "also" "intermediate calculational proof step" K.prf_decl
    1.23 -    (P.marg_comment >> IsarThy.also);
    1.24 +    (calc_args -- P.marg_comment >> IsarThy.also);
    1.25  
    1.26  val finallyP =
    1.27    OuterSyntax.command "finally" "terminal calculational proof step" K.prf_chain
    1.28 -    (P.marg_comment >> IsarThy.finally);
    1.29 +    (calc_args -- P.marg_comment >> IsarThy.finally);
    1.30  
    1.31  
    1.32  (* proof navigation *)
    1.33 @@ -547,10 +554,11 @@
    1.34    print_ast_translationP, token_translationP, oracleP,
    1.35    (*proof commands*)
    1.36    theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
    1.37 -  fixP, letP, thenP, fromP, noteP, beginP, endP, nextP, qed_withP,
    1.38 -  qedP, terminal_proofP, immediate_proofP, default_proofP, applyP,
    1.39 -  then_applyP, proofP, alsoP, finallyP, backP, prevP, upP, topP,
    1.40 -  cannot_undoP, clear_undoP, redoP, undos_proofP, kill_proofP, undoP,
    1.41 +  fixP, letP, thenP, fromP, withP, noteP, beginP, endP, nextP,
    1.42 +  qed_withP, qedP, terminal_proofP, immediate_proofP, default_proofP,
    1.43 +  applyP, then_applyP, proofP, alsoP, finallyP, backP, prevP, upP,
    1.44 +  topP, cannot_undoP, clear_undoP, redoP, undos_proofP, kill_proofP,
    1.45 +  undoP,
    1.46    (*diagnostic commands*)
    1.47    print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
    1.48    print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,