Lines Matching defs:trans
226 fun trans _ s [] = s | trans f s (h::t) = trans f (f h s) t;
257 trans (fn x => C (trans (fn y => f (x, y))) ys') [] xs'
266 trans (fn x => fn y => y ^ ", " ^ elt_to_string x)
388 fun stream_concat ss = trans (C stream_append) (K STREAM_NIL) ss;
397 | tree_size (BRANCH (_, t)) = trans (plus o tree_size) 0 t;
670 val type_vars_in_terms = trans (union o type_vars_in_term) [];
718 val mk_foralls = uncurry (C (trans (curry mk_forall)));
727 val specl = C (trans spec);
897 val eq_th = MK_COMB (REFL pred, trans (C comb_beta) def_th lvars)
1251 val initializel = trans (C initialize_collect)
1267 fun clean_add_thms ths = snd o trans add_thm (map concl ths, ths)