equal
deleted
inserted
replaced
18 |
18 |
19 (**** theory data ****) |
19 (**** theory data ****) |
20 |
20 |
21 fun merge_rules tabs = |
21 fun merge_rules tabs = |
22 Symtab.join (fn _ => fn (ths, ths') => |
22 Symtab.join (fn _ => fn (ths, ths') => |
23 SOME (gen_merge_lists (Drule.eq_thm_prop o pairself fst) ths ths')) tabs; |
23 gen_merge_lists (Drule.eq_thm_prop o pairself fst) ths ths') tabs; |
24 |
24 |
25 structure CodegenData = TheoryDataFun |
25 structure CodegenData = TheoryDataFun |
26 (struct |
26 (struct |
27 val name = "HOL/inductive_codegen"; |
27 val name = "HOL/inductive_codegen"; |
28 type T = |
28 type T = |