--- a/src/Pure/Isar/isar_syn.ML Thu Mar 18 16:44:53 1999 +0100
+++ b/src/Pure/Isar/isar_syn.ML Fri Mar 19 11:24:00 1999 +0100
@@ -33,7 +33,7 @@
(*end current theory / sub-proof / excursion*)
val endP =
- OuterSyntax.command "end" "end current theory / sub-proof / excursion"
+ OuterSyntax.command "end" "end current block / theory / excursion"
(Scan.succeed (Toplevel.print o Toplevel.exit o Toplevel.proof IsarThy.end_block));
val contextP =
@@ -308,42 +308,45 @@
(* end proof *)
-val qedP =
- OuterSyntax.command "qed" "conclude proof"
- (Scan.succeed (Toplevel.proof_to_theory IsarThy.qed));
+val kill_proofP =
+ OuterSyntax.improper_command "kill" "abort current proof"
+ (Scan.succeed (Toplevel.print o Toplevel.proof_to_theory IsarThy.kill_proof));
val qed_withP =
OuterSyntax.improper_command "qed_with" "conclude proof, may patch name and attributes"
- (Scan.option name -- Scan.option attribs >> (Toplevel.proof_to_theory o IsarThy.qed_with));
+ (Scan.option name -- Scan.option attribs -- Scan.option method
+ >> (uncurry IsarThy.global_qed_with));
+
+val qedP =
+ OuterSyntax.command "qed" "conclude (sub-)proof"
+ (Scan.option method >> IsarThy.qed);
-val kill_proofP =
- OuterSyntax.improper_command "kill" "abort current proof"
- (Scan.succeed (Toplevel.print o Toplevel.proof_to_theory IsarThy.kill_proof));
+val terminal_proofP =
+ OuterSyntax.command "by" "terminal backward proof"
+ (method >> (Toplevel.print oo IsarThy.terminal_proof));
+
+val immediate_proofP =
+ OuterSyntax.command "." "immediate proof"
+ (Scan.succeed (Toplevel.print o IsarThy.immediate_proof));
+
+val default_proofP =
+ OuterSyntax.command ".." "default proof"
+ (Scan.succeed (Toplevel.print o IsarThy.default_proof));
(* proof steps *)
-fun gen_stepP meth int name cmt f =
- OuterSyntax.parser int name cmt
- (meth >> (fn txt => Toplevel.print o Toplevel.proof (f txt)));
-
-val stepP = gen_stepP method;
-
-val refineP = stepP true "refine" "unstructured backward proof step, ignoring facts" IsarThy.tac;
-val then_refineP =
- stepP true "then_refine" "unstructured backward proof step, using facts" IsarThy.then_tac;
-
+val refineP =
+ OuterSyntax.improper_command "refine" "unstructured backward proof step, ignoring facts"
+ (method >> (Toplevel.print oo (Toplevel.proof o IsarThy.tac)));
-val proofP = gen_stepP (Scan.option method) false "proof" "backward proof" IsarThy.proof;
-val terminal_proofP = stepP false "by" "terminal backward proof" IsarThy.terminal_proof;
+val then_refineP =
+ OuterSyntax.improper_command "then_refine" "unstructured backward proof step, using facts"
+ (method >> (Toplevel.print oo (Toplevel.proof o IsarThy.then_tac)));
-val immediate_proofP =
- OuterSyntax.command "." "immediate proof"
- (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.immediate_proof));
-
-val default_proofP =
- OuterSyntax.command ".." "default proof"
- (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.default_proof));
+val proofP =
+ OuterSyntax.command "proof" "backward proof"
+ (Scan.option method >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
(* proof history *)
@@ -507,10 +510,10 @@
print_ast_translationP, token_translationP, oracleP,
(*proof commands*)
theoremP, lemmaP, showP, haveP, assumeP, fixP, letP, thenP, fromP,
- factsP, beginP, nextP, qedP, qed_withP, kill_proofP, refineP,
- then_refineP, proofP, terminal_proofP, immediate_proofP,
- default_proofP, clear_undoP, undoP, redoP, undosP, redosP, backP,
- prevP, upP, topP,
+ factsP, beginP, nextP, kill_proofP, qed_withP, qedP,
+ terminal_proofP, immediate_proofP, default_proofP, refineP,
+ then_refineP, proofP, clear_undoP, undoP, redoP, undosP, redosP,
+ backP, prevP, upP, topP,
(*diagnostic commands*)
print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,