Lines Matching defs:defs
601 fun translate_to_c dirname filename defs rewrites main_fun tests =
603 val defs' = (map (SPEC_ALL o (REWRITE_RULE rewrites)) defs)
605 val defined_funs = map extract_fun_const defs';
606 val defs'' = zip (map dest_const defined_funs) defs';
607 val defs'' = Listsort.sort (fn (((s1, _), _), ((s2, _),_)) => String.compare (s1, s2)) defs'';
614 val unknown_consts = get_unknown_consts (map concl defs');
626 val (fun_decl, fun_defs) = unzip (map (fn (_, def) => translate_fun_to_c def) defs'');
628 (* val def = #2 (el 1 defs'');