equal
deleted
inserted
replaced
60 val calculationN = "calculation"; |
60 val calculationN = "calculation"; |
61 |
61 |
62 fun put_calculation calc = |
62 fun put_calculation calc = |
63 `Proof.level #-> (fn lev => Proof.map_context (Context.proof_map |
63 `Proof.level #-> (fn lev => Proof.map_context (Context.proof_map |
64 (CalculationData.map (apsnd (K (Option.map (rpair lev) calc)))))) |
64 (CalculationData.map (apsnd (K (Option.map (rpair lev) calc)))))) |
65 #> Proof.put_thms_internal (calculationN, calc); |
65 #> Proof.put_thms (calculationN, calc); |
66 |
66 |
67 |
67 |
68 |
68 |
69 (** attributes **) |
69 (** attributes **) |
70 |
70 |