src/Pure/Isar/calculation.ML

   val trans_del_global: theory attribute
   val trans_add_local: Proof.context attribute
   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;
 
 structure Calculation: CALCULATION =
 struct

 
 
 
 (** 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 ();
     val facts = Proof.the_facts state;

           |> Proof.reset_thms calculationN
           |> Proof.simple_have_thms "" calc
           |> 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 **)