src/Pure/Isar/calculation.ML
changeset 8562 ce0e2b8e8844
parent 8461 2693a3a9fcc1
child 8588 b7c3f264f8ac
     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