equal
deleted
inserted
replaced
176 (case get_calculation state of |
176 (case get_calculation state of |
177 NONE => (true, Seq.single facts) |
177 NONE => (true, Seq.single facts) |
178 | SOME calc => (false, Seq.map single (combine (calc @ facts)))); |
178 | SOME calc => (false, Seq.map single (combine (calc @ facts)))); |
179 in |
179 in |
180 err_if state (initial andalso final) "No calculation yet"; |
180 err_if state (initial andalso final) "No calculation yet"; |
181 err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given"; |
181 err_if state (initial andalso isSome opt_rules) "Initial calculation -- no rules to be given"; |
182 calculations |> Seq.map (fn calc => (print (Proof.context_of state) calc; |
182 calculations |> Seq.map (fn calc => (print (Proof.context_of state) calc; |
183 state |> maintain_calculation final calc)) |
183 state |> maintain_calculation final calc)) |
184 end; |
184 end; |
185 |
185 |
186 fun also print = calculate false print; |
186 fun also print = calculate false print; |