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