# HG changeset patch
# User wenzelm
# Date 954102671 -7200
# Node ID b7c3f264f8acc4871e78ce097d7002f72c505dd1
# Parent  49069dfedb1e5016df0110a8ce95d3049607a016
added 'ultimately';

diff -r 49069dfedb1e -r b7c3f264f8ac src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Sun Mar 26 22:29:33 2000 +0200
+++ b/src/Pure/Isar/calculation.ML	Sun Mar 26 22:31:11 2000 +0200
@@ -16,6 +16,7 @@
   val also: thm list option -> (thm list -> unit) -> Proof.state -> Proof.state Seq.seq
   val finally: thm list option -> (thm list -> unit) -> Proof.state -> Proof.state Seq.seq
   val moreover: (thm list -> unit) -> Proof.state -> Proof.state
+  val ultimately: (thm list -> unit) -> Proof.state -> Proof.state
   val setup: (theory -> theory) list
 end;
 
@@ -104,22 +105,29 @@
 
 (** proof commands **)
 
-(* maintain calculation *)
+(* maintain calculation register *)
 
 val calculationN = "calculation";
 
-fun maintain_calculation calc state =
-  state
-  |> put_calculation calc
-  |> Proof.simple_have_thms calculationN calc
-  |> Proof.reset_facts;
+fun maintain_calculation false calc state =
+      state
+      |> put_calculation calc
+      |> Proof.simple_have_thms calculationN calc
+      |> Proof.reset_facts
+  | maintain_calculation true calc state =
+      state
+      |> reset_calculation
+      |> Proof.reset_thms calculationN
+      |> Proof.simple_have_thms "" calc
+      |> Proof.chain;
 
 
 (* 'also' and 'finally' *)
 
+fun err_if state b msg = if b then raise Proof.STATE (msg, state) else ();
+
 fun calculate final opt_rules print state =
   let
-    fun err_if b msg = if b then raise Proof.STATE (msg, state) else ();
     val facts = Proof.the_facts state;
 
     val eq_prop = op aconv o pairself (#prop o Thm.rep_thm);
@@ -140,30 +148,33 @@
         None => (true, Seq.single facts)
       | Some thms => (false, Seq.filter (differ thms) (combine thms)))
   in
-    err_if (initial andalso final) "No calculation yet";
-    err_if (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
-    calculations |> Seq.map (fn calc =>
-      (print calc;
-        (if final then
-          state
-          |> reset_calculation
-          |> Proof.reset_thms calculationN
-          |> Proof.simple_have_thms "" calc
-          |> Proof.chain
-        else
-          state
-          |> maintain_calculation calc)))
+    err_if state (initial andalso final) "No calculation yet";
+    err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
+    calculations |> Seq.map (fn calc => (print calc; state |> maintain_calculation final calc))
   end;
 
 fun also print = calculate false print;
 fun finally print = calculate true print;
 
 
-(* 'moreover' *)
+(* 'moreover' and 'ultimately' *)
 
-fun moreover print state =
-  let val calc = if_none (get_calculation state) [] @ Proof.the_facts state
-  in print calc; state |> maintain_calculation calc end;
+fun collect final print state =
+  let
+    val facts = Proof.the_facts state;
+    val (initial, thms) =
+      (case get_calculation state of
+        None => (true, [])
+      | Some thms => (false, thms));
+    val calc = thms @ facts;
+  in
+    err_if state (initial andalso final) "No calculation yet";
+    print calc;
+    state |> maintain_calculation final calc
+  end;
+
+fun moreover print = collect false print;
+fun ultimately print = collect true print;
 
 
 
diff -r 49069dfedb1e -r b7c3f264f8ac src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Mar 26 22:29:33 2000 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sun Mar 26 22:31:11 2000 +0200
@@ -425,6 +425,10 @@
   OuterSyntax.command "moreover" "augment calculation by current facts" K.prf_decl
     (P.marg_comment >> IsarThy.moreover);
 
+val ultimatelyP =
+  OuterSyntax.command "ultimately" "augment calculation by current facts, exhibit result"
+    K.prf_chain (P.marg_comment >> IsarThy.ultimately);
+
 
 (* proof navigation *)
 
@@ -642,8 +646,8 @@
   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, backP, cannot_undoP,
-  clear_undosP, redoP, undos_proofP, undoP, killP,
+  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,
   print_syntaxP, print_theoremsP, print_attributesP, print_methodsP,
diff -r 49069dfedb1e -r b7c3f264f8ac src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Sun Mar 26 22:29:33 2000 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Sun Mar 26 22:31:11 2000 +0200
@@ -144,6 +144,7 @@
   val finally_i: (thm list * Comment.interest) option * Comment.text
     -> Toplevel.transition -> Toplevel.transition
   val moreover: Comment.text -> Toplevel.transition -> Toplevel.transition
+  val ultimately: Comment.text -> Toplevel.transition -> Toplevel.transition
   val parse_ast_translation: string -> theory -> theory
   val parse_translation: string -> theory -> theory
   val print_translation: string -> theory -> theory
@@ -456,6 +457,7 @@
 fun finally x = proof''' (ProofHistory.applys o gen_calc get_thmss Calculation.finally x);
 fun finally_i x = proof''' (ProofHistory.applys o gen_calc get_thmss_i Calculation.finally x);
 fun moreover comment = proof''' (ProofHistory.apply o Calculation.moreover);
+fun ultimately comment = proof''' (ProofHistory.apply o Calculation.ultimately);
 
 end;