Lines Matching defs:thms
7 val thms = DB.match [] ``SPEC ARM_MODEL``
8 val thms = filter (can (find_term (can (match_term ``aLISP``))) o concl) (map (fst o snd) thms)
10 val thms = map renamer thms
12 val _ = add_compiled thms
16 val thms = DB.match [] ``SPEC PPC_MODEL``
17 val thms = filter (can (find_term (can (match_term ``pLISP``))) o concl) (map (fst o snd) thms)
19 val thms = map renamer thms
21 val _ = add_compiled thms
25 val thms = DB.match [] ``SPEC X86_MODEL``
26 val thms = filter (can (find_term (can (match_term ``xLISP``))) o concl) (map (fst o snd) thms)
29 val thms = map renamer thms
31 val _ = add_compiled thms
41 val (thms,_,_) = compile_all ``
436 save_thm("SPEC_lisp_eval_" ^ name ^ "_thm",th)) thms