1.1 --- a/src/Pure/Isar/calculation.ML	Thu Mar 23 21:36:43 2000 +0100
     1.2 +++ b/src/Pure/Isar/calculation.ML	Thu Mar 23 21:37:13 2000 +0100
     1.3 @@ -15,6 +15,7 @@
     1.4    val trans_del_local: Proof.context attribute
     1.5    val also: thm list option -> (thm list -> unit) -> Proof.state -> Proof.state Seq.seq
     1.6    val finally: thm list option -> (thm list -> unit) -> Proof.state -> Proof.state Seq.seq
     1.7 +  val moreover: (thm list -> unit) -> Proof.state -> Proof.state
     1.8    val setup: (theory -> theory) list
     1.9  end;
    1.10  
    1.11 @@ -103,8 +104,19 @@
    1.12  
    1.13  (** proof commands **)
    1.14  
    1.15 +(* maintain calculation *)
    1.16 +
    1.17  val calculationN = "calculation";
    1.18  
    1.19 +fun maintain_calculation calc state =
    1.20 +  state
    1.21 +  |> put_calculation calc
    1.22 +  |> Proof.simple_have_thms calculationN calc
    1.23 +  |> Proof.reset_facts;
    1.24 +
    1.25 +
    1.26 +(* 'also' and 'finally' *)
    1.27 +
    1.28  fun calculate final opt_rules print state =
    1.29    let
    1.30      fun err_if b msg = if b then raise Proof.STATE (msg, state) else ();
    1.31 @@ -140,15 +152,20 @@
    1.32            |> Proof.chain
    1.33          else
    1.34            state
    1.35 -          |> put_calculation calc
    1.36 -          |> Proof.simple_have_thms calculationN calc
    1.37 -          |> Proof.reset_facts)))
    1.38 +          |> maintain_calculation calc)))
    1.39    end;
    1.40  
    1.41  fun also print = calculate false print;
    1.42  fun finally print = calculate true print;
    1.43  
    1.44  
    1.45 +(* 'moreover' *)
    1.46 +
    1.47 +fun moreover print state =
    1.48 +  let val calc = if_none (get_calculation state) [] @ Proof.the_facts state
    1.49 +  in print calc; state |> maintain_calculation calc end;
    1.50 +
    1.51 +
    1.52  
    1.53  (** theory setup **)
    1.54  

     2.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Mar 23 21:36:43 2000 +0100
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Mar 23 21:37:13 2000 +0100
     2.3 @@ -414,13 +414,17 @@
     2.4    Scan.option (P.$$$ "(" |-- P.!!! ((P.xthms1 --| P.$$$ ")") -- P.interest));
     2.5  
     2.6  val alsoP =
     2.7 -  OuterSyntax.command "also" "intermediate calculational proof step" K.prf_decl
     2.8 +  OuterSyntax.command "also" "combine calculation and current facts" K.prf_decl
     2.9      (calc_args -- P.marg_comment >> IsarThy.also);
    2.10  
    2.11  val finallyP =
    2.12 -  OuterSyntax.command "finally" "terminal calculational proof step" K.prf_chain
    2.13 +  OuterSyntax.command "finally" "combine calculation and current facts, exhibit result" K.prf_chain
    2.14      (calc_args -- P.marg_comment >> IsarThy.finally);
    2.15  
    2.16 +val moreoverP =
    2.17 +  OuterSyntax.command "moreover" "augment calculation by current facts" K.prf_decl
    2.18 +    (P.marg_comment >> IsarThy.moreover);
    2.19 +
    2.20  
    2.21  (* proof navigation *)
    2.22  
    2.23 @@ -638,8 +642,8 @@
    2.24    defP, fixP, letP, caseP, thenP, fromP, withP, noteP, beginP, endP,
    2.25    nextP, qedP, terminal_proofP, immediate_proofP, default_proofP,
    2.26    skip_proofP, forget_proofP, deferP, preferP, applyP, apply_endP,
    2.27 -  proofP, alsoP, finallyP, backP, cannot_undoP, clear_undosP, redoP,
    2.28 -  undos_proofP, undoP, killP,
    2.29 +  proofP, alsoP, finallyP, moreoverP, backP, cannot_undoP,
    2.30 +  clear_undosP, redoP, undos_proofP, undoP, killP,
    2.31    (*diagnostic commands*)
    2.32    pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
    2.33    print_syntaxP, print_theoremsP, print_attributesP, print_methodsP,

     3.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Mar 23 21:36:43 2000 +0100
     3.2 +++ b/src/Pure/Isar/isar_thy.ML	Thu Mar 23 21:37:13 2000 +0100
     3.3 @@ -143,6 +143,7 @@
     3.4      -> Toplevel.transition -> Toplevel.transition
     3.5    val finally_i: (thm list * Comment.interest) option * Comment.text
     3.6      -> Toplevel.transition -> Toplevel.transition
     3.7 +  val moreover: Comment.text -> Toplevel.transition -> Toplevel.transition
     3.8    val parse_ast_translation: string -> theory -> theory
     3.9    val parse_translation: string -> theory -> theory
    3.10    val print_translation: string -> theory -> theory
    3.11 @@ -454,6 +455,7 @@
    3.12  fun also_i x = proof''' (ProofHistory.applys o gen_calc get_thmss_i Calculation.also x);
    3.13  fun finally x = proof''' (ProofHistory.applys o gen_calc get_thmss Calculation.finally x);
    3.14  fun finally_i x = proof''' (ProofHistory.applys o gen_calc get_thmss_i Calculation.finally x);
    3.15 +fun moreover comment = proof''' (ProofHistory.apply o Calculation.moreover);
    3.16  
    3.17  end;
    3.18