Lines Matching defs:proofs
3192 val proofs =
3198 ("The type of one or more of the uniqueness proofs: " ^
3203 (proofs,foldl (uncurry PROVE_HYP_CHECK) thm proofs)
3242 fun remove_hyp_terms_pre min pair_thm proofs (mthms,thm) =
3248 val nonpair_rewrites = mapfilter (fn m => tryfind (C MP m) proofs) removed
3262 remove_hyp_terms_pre min pair_thm proofs (map (CONV_RULE conv) kept,PROVE_HYP TRUTH (CONV_HYP conv thm'))
3265 fun remove_hyp_terms pair_thm proofs ([],thm) = thm
3266 | remove_hyp_terms pair_thm proofs (mthms,thm) =
3273 remove_hyp_terms_pre total pair_thm proofs (mthms,thm))
3354 val (proofs,thm') = prove_all_split_terms (get_ind,get_def,conv,create_conv,dead_thm,dead_value) matches thm handle e => wrap e
3355 val thm'' = remove_hyp_terms pair_thm proofs (mthms,thm') handle e => wrap e
3494 (* Polytypic inductive proofs about functions *)
3608 val proofs = map (fn (t,(assums:term list,goal:term)) =>
3620 val sorted = map (fn c => tryfind (C MATCH_IND_TERM c) (hyp thm)) proofs