Lines Matching defs:thms
16 val thms = DB.match [] ``SPEC X64_MODEL``
17 val thms = filter (can (find_term (can (match_term ``zLISP``))) o car o concl) (map (fst o snd) thms)
18 val thms = map (Q.INST [`ddd`|->`SOME F`,`cu`|->`NONE`]) thms
19 val _ = map (fn th => add_compiled [th] handle e => ()) thms
4180 val thms = DB.match [] ``SPEC X64_MODEL``
4181 val thms = filter (can (find_term (can (match_term ``zLISP``))) o car o concl) (map (fst o snd) thms)
4182 val thms = map (Q.INST [`ddd`|->`SOME T`,`cu`|->`NONE`]) thms
4183 val _ = map (fn th => add_compiled [th] handle e => ()) thms
4265 val thms = [SPEC_COMPOSE_RULE [X64_LISP_ERROR_11,X64_LISP_SET_OK_F]]
4266 val thms = map (RW [GSYM no_such_function_bool_def]) thms
4267 val thms = map (Q.INST [`ddd`|->`SOME T`,`cu`|->`NONE`]) thms
4268 val _ = map (fn th => add_compiled [th] handle e => ()) thms
4605 val thms = DB.match [] ``SPEC X64_MODEL``
4606 val thms = filter (can (find_term (can (match_term ``zLISP``))) o car o concl) (map (fst o snd) thms)
4607 val _ = map (fn th => add_compiled [th] handle e => ()) thms