equal
deleted
inserted
replaced
53 val rewr_rules = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq |
53 val rewr_rules = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq |
54 o HOLogic.dest_Trueprop o Thm.concl_of); |
54 o HOLogic.dest_Trueprop o Thm.concl_of); |
55 |
55 |
56 type pred_data = {rel_eq_onp: thm} |
56 type pred_data = {rel_eq_onp: thm} |
57 |
57 |
58 val rel_eq_onp = #rel_eq_onp |
58 val rel_eq_onp: pred_data -> thm = #rel_eq_onp |
59 |
59 |
60 structure Data = Generic_Data |
60 structure Data = Generic_Data |
61 ( |
61 ( |
62 type T = |
62 type T = |
63 { transfer_raw : thm Item_Net.T, |
63 { transfer_raw : thm Item_Net.T, |