src/Pure/Isar/isar_syn.ML
changeset 6404 2daaf2943c79
parent 6370 e71ac23a9111
child 6501 392333eb31cb
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Mar 18 16:44:53 1999 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Mar 19 11:24:00 1999 +0100
     1.3 @@ -33,7 +33,7 @@
     1.4  
     1.5  (*end current theory / sub-proof / excursion*)
     1.6  val endP =
     1.7 -  OuterSyntax.command "end" "end current theory / sub-proof / excursion"
     1.8 +  OuterSyntax.command "end" "end current block / theory / excursion"
     1.9      (Scan.succeed (Toplevel.print o Toplevel.exit o Toplevel.proof IsarThy.end_block));
    1.10  
    1.11  val contextP =
    1.12 @@ -308,42 +308,45 @@
    1.13  
    1.14  (* end proof *)
    1.15  
    1.16 -val qedP =
    1.17 -  OuterSyntax.command "qed" "conclude proof"
    1.18 -    (Scan.succeed (Toplevel.proof_to_theory IsarThy.qed));
    1.19 +val kill_proofP =
    1.20 +  OuterSyntax.improper_command "kill" "abort current proof"
    1.21 +    (Scan.succeed (Toplevel.print o Toplevel.proof_to_theory IsarThy.kill_proof));
    1.22  
    1.23  val qed_withP =
    1.24    OuterSyntax.improper_command "qed_with" "conclude proof, may patch name and attributes"
    1.25 -    (Scan.option name -- Scan.option attribs >> (Toplevel.proof_to_theory o IsarThy.qed_with));
    1.26 +    (Scan.option name -- Scan.option attribs -- Scan.option method
    1.27 +      >> (uncurry IsarThy.global_qed_with));
    1.28 +
    1.29 +val qedP =
    1.30 +  OuterSyntax.command "qed" "conclude (sub-)proof"
    1.31 +    (Scan.option method >> IsarThy.qed);
    1.32  
    1.33 -val kill_proofP =
    1.34 -  OuterSyntax.improper_command "kill" "abort current proof"
    1.35 -    (Scan.succeed (Toplevel.print o Toplevel.proof_to_theory IsarThy.kill_proof));
    1.36 +val terminal_proofP =
    1.37 +  OuterSyntax.command "by" "terminal backward proof"
    1.38 +    (method >> (Toplevel.print oo IsarThy.terminal_proof));
    1.39 +
    1.40 +val immediate_proofP =
    1.41 +  OuterSyntax.command "." "immediate proof"
    1.42 +    (Scan.succeed (Toplevel.print o IsarThy.immediate_proof));
    1.43 +
    1.44 +val default_proofP =
    1.45 +  OuterSyntax.command ".." "default proof"
    1.46 +    (Scan.succeed (Toplevel.print o IsarThy.default_proof));
    1.47  
    1.48  
    1.49  (* proof steps *)
    1.50  
    1.51 -fun gen_stepP meth int name cmt f =
    1.52 -  OuterSyntax.parser int name cmt
    1.53 -    (meth >> (fn txt => Toplevel.print o Toplevel.proof (f txt)));
    1.54 -
    1.55 -val stepP = gen_stepP method;
    1.56 -
    1.57 -val refineP = stepP true "refine" "unstructured backward proof step, ignoring facts" IsarThy.tac;
    1.58 -val then_refineP =
    1.59 -  stepP true "then_refine" "unstructured backward proof step, using facts" IsarThy.then_tac;
    1.60 -
    1.61 +val refineP =
    1.62 +  OuterSyntax.improper_command "refine" "unstructured backward proof step, ignoring facts"
    1.63 +    (method >> (Toplevel.print oo (Toplevel.proof o IsarThy.tac)));
    1.64  
    1.65 -val proofP = gen_stepP (Scan.option method) false "proof" "backward proof" IsarThy.proof;
    1.66 -val terminal_proofP = stepP false "by" "terminal backward proof" IsarThy.terminal_proof;
    1.67 +val then_refineP =
    1.68 +  OuterSyntax.improper_command "then_refine" "unstructured backward proof step, using facts"
    1.69 +    (method >> (Toplevel.print oo (Toplevel.proof o IsarThy.then_tac)));
    1.70  
    1.71 -val immediate_proofP =
    1.72 -  OuterSyntax.command "." "immediate proof"
    1.73 -    (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.immediate_proof));
    1.74 -
    1.75 -val default_proofP =
    1.76 -  OuterSyntax.command ".." "default proof"
    1.77 -    (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.default_proof));
    1.78 +val proofP =
    1.79 +  OuterSyntax.command "proof" "backward proof"
    1.80 +    (Scan.option method >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
    1.81  
    1.82  
    1.83  (* proof history *)
    1.84 @@ -507,10 +510,10 @@
    1.85    print_ast_translationP, token_translationP, oracleP,
    1.86    (*proof commands*)
    1.87    theoremP, lemmaP, showP, haveP, assumeP, fixP, letP, thenP, fromP,
    1.88 -  factsP, beginP, nextP, qedP, qed_withP, kill_proofP, refineP,
    1.89 -  then_refineP, proofP, terminal_proofP, immediate_proofP,
    1.90 -  default_proofP, clear_undoP, undoP, redoP, undosP, redosP, backP,
    1.91 -  prevP, upP, topP,
    1.92 +  factsP, beginP, nextP, kill_proofP, qed_withP, qedP,
    1.93 +  terminal_proofP, immediate_proofP, default_proofP, refineP,
    1.94 +  then_refineP, proofP, clear_undoP, undoP, redoP, undosP, redosP,
    1.95 +  backP, prevP, upP, topP,
    1.96    (*diagnostic commands*)
    1.97    print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
    1.98    print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,