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