GEN_PART_MATCH : (term -> term) -> thm -> term -> thm
GEN_PART_MATCH fn (A |- !x1...xn. t) tm
# let th = ARITH_RULE `m = n ==> m + p = n + p`;; val th : thm = |- m = n ==> m + p = n + p # PART_MATCH lhand th `n:num = p`;; val it : thm = |- n = p ==> n + p = p + p # GEN_PART_MATCH lhand th `n:num = p`;; val it : thm = |- n = p ==> n + p' = p + p'