25 structure Calculation: CALCULATION = |
25 structure Calculation: CALCULATION = |
26 struct |
26 struct |
27 |
27 |
28 (** calculation data **) |
28 (** calculation data **) |
29 |
29 |
30 structure CalculationData = GenericDataFun |
30 structure CalculationData = Generic_Data |
31 ( |
31 ( |
32 type T = (thm Item_Net.T * thm list) * (thm list * int) option; |
32 type T = (thm Item_Net.T * thm list) * (thm list * int) option; |
33 val empty = ((Thm.elim_rules, []), NONE); |
33 val empty = ((Thm.elim_rules, []), NONE); |
34 val extend = I; |
34 val extend = I; |
35 |
35 fun merge (((trans1, sym1), _), ((trans2, sym2), _)) = |
36 fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) = |
|
37 ((Item_Net.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE); |
36 ((Item_Net.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE); |
38 ); |
37 ); |
39 |
38 |
40 fun print_rules ctxt = |
39 fun print_rules ctxt = |
41 let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in |
40 let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in |