Lines Matching defs:thms
260 fun conva thms = DEPTH_CONV (FIRST_CONV (map REWR_CONV thms))
261 fun conv thms thm = CONV_RULE (conva thms) (CONV_HYP (conva thms) thm)
371 val thms = CONJUNCT1 NOT_CLAUSES::
374 val NNF_CONV = TOP_DEPTH_CONV (FIRST_CONV (map REWR_CONV thms));
1296 val thms = map (fn x => backchain_rewrite 0 RR x before trace 3 "\n") terms
1299 (string:string,MATCH_MP thm (LIST_CONJ thms))
1714 val (rmissing,thms) = alpha_match_clauses om clauses
1715 val rthm = hd thms
1726 (rmissing @ lmissing, (INST_TY_TERM match (SPEC_ALL lthm))::thms)
2099 val thms = mapfilter (fn f => f t) [TypeBase.distinct_of,GSYM o TypeBase.distinct_of,
2103 REPEAT (CHANGED_TAC (REWRITE_TAC (thms @ list))) THEN
2227 val thms = map2 (fn l => fn e => ASSUME (mk_eq(mk_comb(e,mk_comb(l,var)),
2230 map (DISCH T o DISCH_ALL o CONV_HYP (PURE_REWRITE_CONV [o_THM])) thms
2273 val thms =
2301 GEN var (DISJ_CASESL nchot (map fix_thm thms))
2374 val (results,thms) = unzip (map2 (fn (n,c) => fn v =>
2405 val thms = mapfilter (fn f => f t)
2411 (case ((Cases THEN REPEAT (CHANGED_TAC (REWRITE_TAC thms)) THEN
2457 val thms = map (fn n => CONV_RULE (bool_EQ_CONV)
2462 AP_TERM encoder (DISJ_CASESL nchot thms)
3646 val (terminals,thms) = unzip (map2 rc all_detectors funcs)
3651 funcs (map concl thms)
3653 (props,thms,output_terms)
3942 val (singles,(thms,defs)) =
4042 val (props,thms,terms) = create_abstract_recognizers fname f target t
4053 val theorems = map (CONV_RULE conv) thms;