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