IPSPEC : (term -> thm -> thm)

- STRUCTURE
- LIBRARY
- pair
- SYNOPSIS
- Specializes a theorem, with type instantiation if necessary.
- DESCRIPTION
- This rule specializes a paired quantification as does PSPEC; it differs from it in also instantiating the type if needed:(where q is free for p in tm, and ty' is an instance of ty).
A |- !p:ty.tm ----------------------- IPSPEC "q:ty'" A |- tm[q/p]

- FAILURE
- IPSPEC fails if the input theorem is not universally quantified, if the type of the given term is not an instance of the type of the quantified variable, or if the type variable is free in the assumptions.
- SEEALSO

HOL Kananaskis-14