Specialize
Thm.Specialize : term -> thm -> thm
Specializes the conclusion of a universal theorem.
When applied to a term u and a theorem A |- !x. t, Specialize
returns the theorem A |- t[u/x]. Care is taken to ensure that no
variables free in u become bound after this operation.
A |- !x. t
-------------- Specialize u
A |- t[u/x]
Failure
Fails if the theorem's conclusion is not universally quantified, or if
x and u have different types.
Comments
Specialize behaves identically to SPEC, but is faster.
See also
Thm.SPEC, Drule.ISPEC,
Drule.SPECL, Drule.SPEC_ALL,
Drule.SPEC_VAR, Thm.GEN,
Thm.GENL, Drule.GEN_ALL