equal
deleted
inserted
replaced
69 val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.insert); |
69 val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.insert); |
70 val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.delete); |
70 val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.delete); |
71 |
71 |
72 val sym_add = |
72 val sym_add = |
73 Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.add_thm) |
73 Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.add_thm) |
74 #> ContextRules.elim_query NONE; |
74 #> Context_Rules.elim_query NONE; |
|
75 |
75 val sym_del = |
76 val sym_del = |
76 Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.del_thm) |
77 Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.del_thm) |
77 #> ContextRules.rule_del; |
78 #> Context_Rules.rule_del; |
78 |
79 |
79 |
80 |
80 (* symmetric *) |
81 (* symmetric *) |
81 |
82 |
82 val symmetric = Thm.rule_attribute (fn x => fn th => |
83 val symmetric = Thm.rule_attribute (fn x => fn th => |