src/Pure/Isar/calculation.ML
changeset 7600 73f91da46230
parent 7554 30327f9f6b4a
child 8150 7021549ef32d
equal deleted inserted replaced
7599:40b7f7f51208 7600:73f91da46230
   140     calculations |> Seq.map (fn calc =>
   140     calculations |> Seq.map (fn calc =>
   141       (print calc;
   141       (print calc;
   142         (if final then
   142         (if final then
   143           state
   143           state
   144           |> reset_calculation
   144           |> reset_calculation
   145           |> Proof.simple_have_thms calculationN []
   145           |> Proof.reset_thms calculationN
   146           |> Proof.simple_have_thms "" calc
   146           |> Proof.simple_have_thms "" calc
   147           |> Proof.chain
   147           |> Proof.chain
   148         else
   148         else
   149           state
   149           state
   150           |> put_calculation calc
   150           |> put_calculation calc