added "done" proof;

--- a/src/Pure/Isar/isar_syn.ML	Wed May 24 19:09:36 2000 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed May 24 19:09:50 2000 +0200
@@ -371,13 +371,17 @@
     (P.method -- P.interest -- Scan.option (P.method -- P.interest)
       -- P.marg_comment >> IsarThy.terminal_proof);
 
+val default_proofP =
+  OuterSyntax.command ".." "default proof" K.qed
+    (P.marg_comment >> IsarThy.default_proof);
+
 val immediate_proofP =
   OuterSyntax.command "." "immediate proof" K.qed
     (P.marg_comment >> IsarThy.immediate_proof);
 
-val default_proofP =
-  OuterSyntax.command ".." "default proof" K.qed
-    (P.marg_comment >> IsarThy.default_proof);
+val done_proofP =
+  OuterSyntax.command "done" "done proof" K.qed
+    (P.marg_comment >> IsarThy.done_proof);
 
 val skip_proofP =
   OuterSyntax.improper_command "sorry" "skip proof (quick-and-dirty mode only!)" K.qed
@@ -648,9 +652,9 @@
   (*proof commands*)
   theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
   defP, fixP, letP, caseP, thenP, fromP, withP, noteP, beginP, endP,
-  nextP, qedP, terminal_proofP, immediate_proofP, default_proofP,
-  skip_proofP, forget_proofP, deferP, preferP, applyP, apply_endP,
-  proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
+  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,
   (*diagnostic commands*)
   pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,

--- a/src/Pure/Isar/isar_thy.ML	Wed May 24 19:09:36 2000 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Wed May 24 19:09:50 2000 +0200
@@ -135,8 +135,9 @@
     -> Toplevel.transition -> Toplevel.transition
   val terminal_proof: ((Method.text * Comment.interest) * (Method.text * Comment.interest) option)
     * Comment.text -> Toplevel.transition -> Toplevel.transition
+  val default_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
   val immediate_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
-  val default_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
+  val done_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
   val skip_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
   val forget_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
   val get_thmss: (string * Args.src list) list -> Proof.state -> thm list
@@ -438,16 +439,17 @@
 (* local endings *)
 
 val local_qed =
-  proof'' o (ProofHistory.applys oo Method.local_qed) o apsome Comment.ignore_interest;
+  proof'' o (ProofHistory.applys oo Method.local_qed true) o apsome Comment.ignore_interest;
 
 fun ignore_interests (x, y) = (Comment.ignore_interest x, apsome Comment.ignore_interest y);
 
 val local_terminal_proof =
   proof'' o (ProofHistory.applys oo Method.local_terminal_proof) o ignore_interests;
 
+val local_default_proof = proof'' (ProofHistory.applys o Method.local_default_proof);
 val local_immediate_proof = proof'' (ProofHistory.applys o Method.local_immediate_proof);
-val local_default_proof = proof'' (ProofHistory.applys o Method.local_default_proof);
 val local_skip_proof = proof'' (ProofHistory.applys o SkipProof.local_skip_proof);
+val local_done_proof = proof'' (ProofHistory.applys o Method.local_done_proof);
 
 
 (* global endings *)
@@ -459,19 +461,21 @@
     val (thy, res as {kind, name, thm}) = finish state;
   in print_result res; Context.setmp (Some thy) (Present.result kind name) thm; thy end);
 
-val global_qed = global_result o Method.global_qed o apsome Comment.ignore_interest;
+val global_qed = global_result o Method.global_qed true o apsome Comment.ignore_interest;
 val global_terminal_proof = global_result o Method.global_terminal_proof o ignore_interests;
+val global_default_proof = global_result Method.global_default_proof;
 val global_immediate_proof = global_result Method.global_immediate_proof;
-val global_default_proof = global_result Method.global_default_proof;
 val global_skip_proof = global_result SkipProof.global_skip_proof;
+val global_done_proof = global_result Method.global_done_proof;
 
 
 (* common endings *)
 
 fun qed (meth, comment) = local_qed meth o global_qed meth;
 fun terminal_proof (meths, comment) = local_terminal_proof meths o global_terminal_proof meths;
+fun default_proof comment = local_default_proof o global_default_proof;
 fun immediate_proof comment = local_immediate_proof o global_immediate_proof;
-fun default_proof comment = local_default_proof o global_default_proof;
+fun done_proof comment = local_done_proof o global_done_proof;
 fun skip_proof comment = local_skip_proof o global_skip_proof;
 
 fun forget_proof comment = Toplevel.proof_to_theory (Proof.theory_of o ProofHistory.current);

--- a/src/Pure/Isar/method.ML	Wed May 24 19:09:36 2000 +0200
+++ b/src/Pure/Isar/method.ML	Wed May 24 19:09:50 2000 +0200
@@ -86,21 +86,25 @@
   val refine: text -> Proof.state -> Proof.state Seq.seq
   val refine_end: text -> Proof.state -> Proof.state Seq.seq
   val proof: text option -> Proof.state -> Proof.state Seq.seq
-  val local_qed: text option
+  val local_qed: bool -> text option
     -> ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
     -> Proof.state -> Proof.state Seq.seq
   val local_terminal_proof: text * text option
     -> ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
     -> Proof.state -> Proof.state Seq.seq
-  val local_immediate_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
-    -> Proof.state -> Proof.state Seq.seq
   val local_default_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
     -> Proof.state -> Proof.state Seq.seq
-  val global_qed: text option -> Proof.state -> theory * {kind: string, name: string, thm: thm}
+  val local_immediate_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
+    -> Proof.state -> Proof.state Seq.seq
+  val local_done_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
+    -> Proof.state -> Proof.state Seq.seq
+  val global_qed: bool -> text option
+    -> Proof.state -> theory * {kind: string, name: string, thm: thm}
   val global_terminal_proof: text * text option
     -> Proof.state -> theory * {kind: string, name: string, thm: thm}
+  val global_default_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
   val global_immediate_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
-  val global_default_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
+  val global_done_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
   val setup: (theory -> theory) list
 end;
 
@@ -202,7 +206,7 @@
 val METHOD = Proof.method;
 val METHOD_CASES = Proof.method_cases;
 
-fun METHOD0 tac = METHOD (fn [] => tac | _ => error "Method may not be used with facts");
+fun METHOD0 tac = METHOD (fn [] => tac | _ => error "Cannot handle current facts");
 
 
 (* primitive *)
@@ -536,11 +540,13 @@
 
 val default_text = Source (Args.src (("default", []), Position.none));
 val this_text = Basic (K this);
-
-fun finish ctxt = METHOD (K (FILTER Thm.no_prems (ALLGOALS (assm_tac ctxt) THEN flexflex_tac)));
+val done_text = Basic (K (METHOD0 all_tac));
 
-fun finish_text None = Basic finish
-  | finish_text (Some txt) = Then [txt, Basic finish];
+fun close_text asm = Basic (fn ctxt => METHOD (K
+  (FILTER Thm.no_prems ((if asm then ALLGOALS (assm_tac ctxt) else all_tac) THEN flexflex_tac))));
+
+fun finish_text asm None = close_text asm
+  | finish_text asm (Some txt) = Then [txt, close_text asm];
 
 fun proof opt_text state =
   state
@@ -549,31 +555,34 @@
   |> Seq.map (Proof.goal_facts (K []))
   |> Seq.map Proof.enter_forward;
 
-fun local_qed opt_text = Proof.local_qed (refine (finish_text opt_text));
-fun local_terminal_proof (text, opt_text) pr = Seq.THEN (proof (Some text), local_qed opt_text pr);
+fun local_qed asm opt_text = Proof.local_qed (refine (finish_text asm opt_text));
+fun local_terminal_proof (text, opt_text) pr =
+  Seq.THEN (proof (Some text), local_qed true opt_text pr);
+val local_default_proof = local_terminal_proof (default_text, None);
 val local_immediate_proof = local_terminal_proof (this_text, None);
-val local_default_proof = local_terminal_proof (default_text, None);
+fun local_done_proof pr = Seq.THEN (proof (Some done_text), local_qed false None pr);
 
 
-fun global_qeds opt_text = Proof.global_qed (refine (finish_text opt_text));
+fun global_qeds asm opt_text = Proof.global_qed (refine (finish_text asm opt_text));
 
-fun global_qed opt_text state =
+fun global_qed asm opt_text state =
   state
-  |> global_qeds opt_text
+  |> global_qeds asm opt_text
   |> Proof.check_result "Failed to finish proof" state
   |> Seq.hd;
 
-fun global_terminal_proof (text, opt_text) state =
+fun global_term_proof asm (text, opt_text) state =
   state
   |> proof (Some text)
   |> Proof.check_result "Terminal proof method failed" state
-  |> (Seq.flat o Seq.map (global_qeds opt_text))
+  |> (Seq.flat o Seq.map (global_qeds asm opt_text))
   |> Proof.check_result "Failed to finish proof (after successful terminal method)" state
   |> Seq.hd;
 
-val global_immediate_proof = global_terminal_proof (this_text, None);
+val global_terminal_proof = global_term_proof true;
 val global_default_proof = global_terminal_proof (default_text, None);
-
+val global_immediate_proof = global_terminal_proof (this_text, None);
+val global_done_proof = global_term_proof false (done_text, None);
 
 
 (** theory setup **)