Lines Matching defs:func
81 val func = INST_TYPE[alpha|->ty, beta|->self]
83 inj_pair = func (#inj_pair constantly_rich),
84 ret_map = func (#ret_map constantly_rich),
86 all_thm = func (#all_thm constantly_rich),
87 all_map = func (#all_map constantly_rich),
88 all_T = func (#all_T constantly_rich),
89 all_mono = func (#all_mono constantly_rich)
204 val func = fn (x,l) => RIGHT_LIST_BETA (REFL (list_mk_comb(list_mk_abs(l, x), l)))
205 val r' = func(r, rets)
206 val m' = func(m, maps)
241 val func = fn (w, (x, (y, z))) => gen_rich_tyvar w x y z
242 val rtcs = map func
388 val func = fn x => (PURE_REWRITE_RULE [mythm] x
392 ((fst o dest_const o #all_tm) x, func (#all_mono x)))
406 val func = fn (s,ax) => define_new_type_bijections
408 in map func (zip ty_names tyaxs)