# HG changeset patch
# User wenzelm
# Date 953843833 -3600
# Node ID ce0e2b8e88446576d4c7d57c67a80d0dc0593cf1
# Parent  2675e2f4dc61200cbe9ae386e91bbfcd6ecf38ab
added 'moreover' command;

diff -r 2675e2f4dc61 -r ce0e2b8e8844 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Thu Mar 23 21:36:43 2000 +0100
+++ b/src/Pure/Isar/calculation.ML	Thu Mar 23 21:37:13 2000 +0100
@@ -15,6 +15,7 @@
   val trans_del_local: Proof.context attribute
   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 setup: (theory -> theory) list
 end;
 
@@ -103,8 +104,19 @@
 
 (** proof commands **)
 
+(* maintain calculation *)
+
 val calculationN = "calculation";
 
+fun maintain_calculation calc state =
+  state
+  |> put_calculation calc
+  |> Proof.simple_have_thms calculationN calc
+  |> Proof.reset_facts;
+
+
+(* 'also' and 'finally' *)
+
 fun calculate final opt_rules print state =
   let
     fun err_if b msg = if b then raise Proof.STATE (msg, state) else ();
@@ -140,15 +152,20 @@
           |> Proof.chain
         else
           state
-          |> put_calculation calc
-          |> Proof.simple_have_thms calculationN calc
-          |> Proof.reset_facts)))
+          |> maintain_calculation calc)))
   end;
 
 fun also print = calculate false print;
 fun finally print = calculate true print;
 
 
+(* 'moreover' *)
+
+fun moreover print state =
+  let val calc = if_none (get_calculation state) [] @ Proof.the_facts state
+  in print calc; state |> maintain_calculation calc end;
+
+
 
 (** theory setup **)
 
diff -r 2675e2f4dc61 -r ce0e2b8e8844 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Mar 23 21:36:43 2000 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Mar 23 21:37:13 2000 +0100
@@ -414,13 +414,17 @@
   Scan.option (P.$$$ "(" |-- P.!!! ((P.xthms1 --| P.$$$ ")") -- P.interest));
 
 val alsoP =
-  OuterSyntax.command "also" "intermediate calculational proof step" K.prf_decl
+  OuterSyntax.command "also" "combine calculation and current facts" K.prf_decl
     (calc_args -- P.marg_comment >> IsarThy.also);
 
 val finallyP =
-  OuterSyntax.command "finally" "terminal calculational proof step" K.prf_chain
+  OuterSyntax.command "finally" "combine calculation and current facts, exhibit result" K.prf_chain
     (calc_args -- P.marg_comment >> IsarThy.finally);
 
+val moreoverP =
+  OuterSyntax.command "moreover" "augment calculation by current facts" K.prf_decl
+    (P.marg_comment >> IsarThy.moreover);
+
 
 (* proof navigation *)
 
@@ -638,8 +642,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, backP, cannot_undoP, clear_undosP, redoP,
-  undos_proofP, undoP, killP,
+  proofP, alsoP, finallyP, moreoverP, 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 2675e2f4dc61 -r ce0e2b8e8844 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Thu Mar 23 21:36:43 2000 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Thu Mar 23 21:37:13 2000 +0100
@@ -143,6 +143,7 @@
     -> Toplevel.transition -> Toplevel.transition
   val finally_i: (thm list * Comment.interest) option * Comment.text
     -> Toplevel.transition -> Toplevel.transition
+  val moreover: 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
@@ -454,6 +455,7 @@
 fun also_i x = proof''' (ProofHistory.applys o gen_calc get_thmss_i Calculation.also x);
 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);
 
 end;