src/Pure/Isar/calculation.ML
changeset 6877 3d5e5e6f9e20
parent 6787 25265c6807c3
child 6903 682f8a9ec75d
     1.1 --- a/src/Pure/Isar/calculation.ML	Thu Jul 01 21:20:57 1999 +0200
     1.2 +++ b/src/Pure/Isar/calculation.ML	Thu Jul 01 21:25:58 1999 +0200
     1.3 @@ -13,8 +13,8 @@
     1.4    val trans_del_global: theory attribute
     1.5    val trans_add_local: Proof.context attribute
     1.6    val trans_del_local: Proof.context attribute
     1.7 -  val also: (thm -> unit) -> Proof.state -> Proof.state Seq.seq
     1.8 -  val finally: (thm -> unit) -> Proof.state -> Proof.state Seq.seq
     1.9 +  val also: thm list option -> (thm -> unit) -> Proof.state -> Proof.state Seq.seq
    1.10 +  val finally: thm list option -> (thm -> unit) -> Proof.state -> Proof.state Seq.seq
    1.11    val setup: (theory -> theory) list
    1.12  end;
    1.13  
    1.14 @@ -27,7 +27,6 @@
    1.15  fun print_rules ths =
    1.16    Pretty.writeln (Pretty.big_list "calculation rules:" (map Display.pretty_thm ths));
    1.17  
    1.18 -
    1.19  (* theory data kind 'Isar/calculation' *)
    1.20  
    1.21  structure GlobalCalculationArgs =
    1.22 @@ -117,14 +116,12 @@
    1.23  
    1.24  (** proof commands **)
    1.25  
    1.26 -fun have_thms name thms = Proof.have_thmss name [] [(thms, [])];
    1.27 -
    1.28  val calculationN = "calculation";
    1.29  
    1.30 -fun calculate final print state =
    1.31 +fun calculate final opt_rules print state =
    1.32    let
    1.33      val fact = Proof.the_fact state;
    1.34 -    val rules = Seq.of_list (get_local_rules state);
    1.35 +    val rules = Seq.of_list (case opt_rules of None => get_local_rules state | Some thms => thms);
    1.36      val calculations =
    1.37        (case get_calculation state of
    1.38          None => Seq.single fact
    1.39 @@ -135,13 +132,13 @@
    1.40          (if final then
    1.41            state
    1.42            |> reset_calculation
    1.43 -          |> have_thms calculationN []
    1.44 -          |> have_thms "" [calc]
    1.45 +          |> Proof.simple_have_thms calculationN []
    1.46 +          |> Proof.simple_have_thms "" [calc]
    1.47            |> Proof.chain
    1.48          else
    1.49            state
    1.50            |> put_calculation calc
    1.51 -          |> have_thms calculationN [calc]
    1.52 +          |> Proof.simple_have_thms calculationN [calc]
    1.53            |> Proof.reset_facts)))
    1.54    end;
    1.55