equal
deleted
inserted
replaced
151 fun maintain_calculation false calc = put_calculation (SOME calc) |
151 fun maintain_calculation false calc = put_calculation (SOME calc) |
152 | maintain_calculation true calc = put_calculation NONE #> Proof.chain_facts calc; |
152 | maintain_calculation true calc = put_calculation NONE #> Proof.chain_facts calc; |
153 |
153 |
154 fun print_calculation false _ _ = () |
154 fun print_calculation false _ _ = () |
155 | print_calculation true ctxt calc = |
155 | print_calculation true ctxt calc = |
156 Pretty.writeln (Pretty.big_list "calculation:" (map (ProofContext.pretty_thm ctxt) calc)); |
|
157 (* FIXME |
|
158 Pretty.writeln (ProofContext.pretty_fact ctxt (calculationN, calc)); |
156 Pretty.writeln (ProofContext.pretty_fact ctxt (calculationN, calc)); |
159 *) |
|
160 |
157 |
161 |
158 |
162 (* also and finally *) |
159 (* also and finally *) |
163 |
160 |
164 fun calculate prep_rules final raw_rules int state = |
161 fun calculate prep_rules final raw_rules int state = |