SPEC_TAC : term * term -> tactic

- STRUCTURE
- SYNOPSIS
- Generalizes a goal.
- DESCRIPTION
- When applied to a pair of terms (u,x), where x is just a variable, and a goal A ?- t, the tactic SPEC_TAC generalizes the goal to A ?- !x. t[x/u], that is, all instances of u are turned into x.
A ?- t ================= SPEC_TAC (u,x) A ?- !x. t[x/u]

- FAILURE
- Fails unless x is a variable with the same type as u.
- USES
- Removing unnecessary speciality in a goal, particularly as a prelude to an inductive proof.
- SEEALSO

HOL Kananaskis-14