Lines Matching defs:thms
663 | LIST_MK_CONJ thms = LMC thms handle e => wrapException "LIST_MK_CONJ" e
687 fun TC_THMS thms =
688 let val next = trans_all thms thms
689 val diff = op_set_diff (fn a => fn b => concl a = concl b) next thms
691 if null diff then thms else TC_THMS (diff @ thms)
1744 | fix_thms thms clause induction =
1749 val thms' = map (fn t => tryfind_e Empty (C (PART_MATCH (fst o dest_imp_only)) t) thms handle Empty =>
1751 val final = foldr (fn (a,t) => MATCH_MP MONO_AND (CONJ a t)) (last thms') (butlast thms')
3089 | mk_all_extra thms =
3091 of SOME assum => map (RIGHT_CONV_RULE (REPEATC (CHANGED_CONV (PURE_ONCE_REWRITE_CONV [dead_thm,ASSUME assum,COND_CLAUSES] THENC PURE_ONCE_REWRITE_CONV thms)))) thms
3646 val (thms,failed) = mappartition (fn t =>
3656 app (fn (t,thm) => add_coding_theorem_precise target t name thm) thms
3676 val thms = map (fn t => (t,first (can (match_term (mk_conc t)) o concl) (CONJUNCTS thm))) split_types;
3677 val (thms,failed) = mappartition (fn t =>
3688 app (fn (t,thm) => add_source_theorem_precise t name thm) thms