equal
deleted
inserted
replaced
113 fun maintain_calculation false calc = put_calculation (SOME calc) |
113 fun maintain_calculation false calc = put_calculation (SOME calc) |
114 | maintain_calculation true calc = put_calculation NONE #> Proof.chain_facts calc; |
114 | maintain_calculation true calc = put_calculation NONE #> Proof.chain_facts calc; |
115 |
115 |
116 fun print_calculation false _ _ = () |
116 fun print_calculation false _ _ = () |
117 | print_calculation true ctxt calc = Pretty.writeln |
117 | print_calculation true ctxt calc = Pretty.writeln |
118 (ProofContext.pretty_fact ctxt (ProofContext.full_name ctxt calculationN, calc)); |
118 (ProofContext.pretty_fact ctxt (ProofContext.full_bname ctxt calculationN, calc)); |
119 |
119 |
120 |
120 |
121 (* also and finally *) |
121 (* also and finally *) |
122 |
122 |
123 val get_rules = #1 o CalculationData.get o Context.Proof o Proof.context_of; |
123 val get_rules = #1 o CalculationData.get o Context.Proof o Proof.context_of; |