equal
deleted
inserted
replaced
95 val name = "HOL/inductive"; |
95 val name = "HOL/inductive"; |
96 type T = inductive_info Symtab.table * thm list; |
96 type T = inductive_info Symtab.table * thm list; |
97 |
97 |
98 val empty = (Symtab.empty, []); |
98 val empty = (Symtab.empty, []); |
99 val copy = I; |
99 val copy = I; |
100 val finish = I; |
|
101 val prep_ext = I; |
100 val prep_ext = I; |
102 fun merge ((tab1, monos1), (tab2, monos2)) = |
101 fun merge ((tab1, monos1), (tab2, monos2)) = |
103 (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2)); |
102 (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2)); |
104 |
103 |
105 fun print sg (tab, monos) = |
104 fun print sg (tab, monos) = |