Lines Matching defs:thms
19 fun add_code_abbrev thms = (code_abbreviations := thms @ !code_abbreviations);
65 print_cfg (construct_thm_trace thms)
78 fun construct_thm_trace thms = let
110 val xs = list_lookup p thms
327 fun inst_pc_var tools thms = let
348 in map (triple_apply f) thms end
577 fun inst_pc_rel_const tools thms code = let
596 in map (triple_apply foo) thms end
606 fun abbreviate_code name thms = let
608 val cs = map extract_code thms
613 val (_,(th,_,_),_) = hd thms
640 val thms = map (triple_apply foo) thms
642 in (code_def,thms) end
681 val thms = snd (derive_individual_specs code)
683 if length thms = 0 then [] else
684 find_stack_accesses sec_name thms
687 val thms = try_map (fn (n,_,_) => add_stack_intro_fail n sec_name)
688 (apply_thms (STACK_INTRO_RULE stack_accesses)) thms
690 val (code_abbrev_def, thms) =
691 if length thms = 0 then (TRUTH, thms) else
692 abbreviate_code sec_name thms
693 in thms end;