src/Pure/Isar/isar_syn.ML
changeset 8235 a4fb9be6b19a
parent 8227 d67db92897df
child 8349 611342539639
equal deleted inserted replaced
8234:36a85a6c4852 8235:a4fb9be6b19a
   389 
   389 
   390 
   390 
   391 (* proof steps *)
   391 (* proof steps *)
   392 
   392 
   393 val deferP =
   393 val deferP =
   394   OuterSyntax.improper_command "defer" "shuffle internal proof state"
   394   OuterSyntax.command "defer" "shuffle internal proof state"
   395     K.prf_script (Scan.option P.nat >> (Toplevel.print oo (Toplevel.proof o IsarThy.defer)));
   395     K.prf_script (Scan.option P.nat >> (Toplevel.print oo (Toplevel.proof o IsarThy.defer)));
   396 
   396 
   397 val preferP =
   397 val preferP =
   398   OuterSyntax.improper_command "prefer" "shuffle internal proof state"
   398   OuterSyntax.command "prefer" "shuffle internal proof state"
   399     K.prf_script (P.nat >> (Toplevel.print oo (Toplevel.proof o IsarThy.prefer)));
   399     K.prf_script (P.nat >> (Toplevel.print oo (Toplevel.proof o IsarThy.prefer)));
   400 
   400 
   401 val applyP =
   401 val applyP =
   402   OuterSyntax.improper_command "apply" "unstructured backward proof step, ignoring facts"
   402   OuterSyntax.command "apply" "initial refinement step (unstructured)"
   403     K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.tac)));
   403     K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.apply)));
   404 
   404 
   405 val then_applyP =
   405 val apply_endP =
   406   OuterSyntax.improper_command "then_apply" "unstructured backward proof step, using facts"
   406   OuterSyntax.command "apply_end" "terminal refinement (unstructured)"
   407     K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.then_tac)));
   407     K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.apply_end)));
   408 
   408 
   409 val proofP =
   409 val proofP =
   410   OuterSyntax.command "proof" "backward proof" K.prf_block
   410   OuterSyntax.command "proof" "backward proof" K.prf_block
   411     (P.interest -- Scan.option (P.method -- P.interest) -- P.marg_comment
   411     (P.interest -- Scan.option (P.method -- P.interest) -- P.marg_comment
   412       >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
   412       >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
   427 
   427 
   428 
   428 
   429 (* proof navigation *)
   429 (* proof navigation *)
   430 
   430 
   431 val backP =
   431 val backP =
   432   OuterSyntax.improper_command "back" "backtracking of proof command" K.prf_script
   432   OuterSyntax.command "back" "backtracking of proof command" K.prf_script
   433     (Scan.optional (P.$$$ "!" >> K true) false >>
   433     (Scan.optional (P.$$$ "!" >> K true) false >>
   434       (Toplevel.print oo (Toplevel.proof o ProofHistory.back)));
   434       (Toplevel.print oo (Toplevel.proof o ProofHistory.back)));
   435 
   435 
   436 
   436 
   437 (* history *)
   437 (* history *)
   631   print_ast_translationP, token_translationP, oracleP,
   631   print_ast_translationP, token_translationP, oracleP,
   632   (*proof commands*)
   632   (*proof commands*)
   633   theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
   633   theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
   634   defP, fixP, letP, thenP, thenceP, fromP, withP, noteP, beginP, endP,
   634   defP, fixP, letP, thenP, thenceP, fromP, withP, noteP, beginP, endP,
   635   nextP, qedP, terminal_proofP, immediate_proofP, default_proofP,
   635   nextP, qedP, terminal_proofP, immediate_proofP, default_proofP,
   636   skip_proofP, forget_proofP, deferP, preferP, applyP, then_applyP,
   636   skip_proofP, forget_proofP, deferP, preferP, applyP, apply_endP,
   637   proofP, alsoP, finallyP, backP, cannot_undoP, clear_undosP, redoP,
   637   proofP, alsoP, finallyP, backP, cannot_undoP, clear_undosP, redoP,
   638   undos_proofP, kill_proofP, undoP,
   638   undos_proofP, kill_proofP, undoP,
   639   (*diagnostic commands*)
   639   (*diagnostic commands*)
   640   pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
   640   pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
   641   print_syntaxP, print_theoremsP, print_attributesP, print_methodsP,
   641   print_syntaxP, print_theoremsP, print_attributesP, print_methodsP,