equal
deleted
inserted
replaced
56 in |
56 in |
57 { add_simps = add_simps, case_names = case_names, |
57 { add_simps = add_simps, case_names = case_names, |
58 fs = map term fs, R = term R, psimps = fact psimps, |
58 fs = map term fs, R = term R, psimps = fact psimps, |
59 pinducts = fact pinducts, simps = Option.map fact simps, |
59 pinducts = fact pinducts, simps = Option.map fact simps, |
60 inducts = Option.map fact inducts, termination = thm termination, |
60 inducts = Option.map fact inducts, termination = thm termination, |
61 defname = name defname, is_partial=is_partial, eqvts = (*fact*) eqvts } |
61 defname = name defname, is_partial=is_partial, eqvts = fact eqvts } |
62 end |
62 end |
63 |
63 |
64 structure NominalFunctionData = Generic_Data |
64 structure NominalFunctionData = Generic_Data |
65 ( |
65 ( |
66 type T = (term * nominal_info) Item_Net.T; |
66 type T = (term * nominal_info) Item_Net.T; |