mathlib documentation

tactic.generalize_proofs

source
meta def tactic.generalize_proofs (ns : list name) :
tactic unit

source
meta def tactic.interactive.generalize_proofs (a : interactive.parse interactive.types.ident_ * ) :
tactic unit

Generalize proofs in the goal, naming them with the provided list.