equal
deleted
inserted
replaced
33 type T = (thm NetRules.T * thm list) * (thm list * int) option; |
33 type T = (thm NetRules.T * thm list) * (thm list * int) option; |
34 val empty = ((NetRules.elim, []), NONE); |
34 val empty = ((NetRules.elim, []), NONE); |
35 val extend = I; |
35 val extend = I; |
36 |
36 |
37 fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) = |
37 fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) = |
38 ((NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2)), NONE); |
38 ((NetRules.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE); |
39 ); |
39 ); |
40 |
40 |
41 fun print_rules ctxt = |
41 fun print_rules ctxt = |
42 let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in |
42 let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in |
43 [Pretty.big_list "transitivity rules:" |
43 [Pretty.big_list "transitivity rules:" |
69 |
69 |
70 val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.insert); |
70 val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.insert); |
71 val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.delete); |
71 val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.delete); |
72 |
72 |
73 val sym_add = |
73 val sym_add = |
74 Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Drule.add_rule) |
74 Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.add_thm) |
75 #> ContextRules.elim_query NONE; |
75 #> ContextRules.elim_query NONE; |
76 val sym_del = |
76 val sym_del = |
77 Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Drule.del_rule) |
77 Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.del_thm) |
78 #> ContextRules.rule_del; |
78 #> ContextRules.rule_del; |
79 |
79 |
80 |
80 |
81 (* symmetric *) |
81 (* symmetric *) |
82 |
82 |