equal
deleted
inserted
replaced
31 type calculation = {result: thm list, level: int, serial: serial, pos: Position.T}; |
31 type calculation = {result: thm list, level: int, serial: serial, pos: Position.T}; |
32 |
32 |
33 structure Data = Generic_Data |
33 structure Data = Generic_Data |
34 ( |
34 ( |
35 type T = (thm Item_Net.T * thm Item_Net.T) * calculation option; |
35 type T = (thm Item_Net.T * thm Item_Net.T) * calculation option; |
36 val empty = ((Thm.elim_rules, Thm.full_rules), NONE); |
36 val empty = ((Thm.item_net_elim, Thm.item_net), NONE); |
37 val extend = I; |
37 val extend = I; |
38 fun merge (((trans1, sym1), _), ((trans2, sym2), _)) = |
38 fun merge (((trans1, sym1), _), ((trans2, sym2), _)) = |
39 ((Item_Net.merge (trans1, trans2), Item_Net.merge (sym1, sym2)), NONE); |
39 ((Item_Net.merge (trans1, trans2), Item_Net.merge (sym1, sym2)), NONE); |
40 ); |
40 ); |
41 |
41 |