AP_THM : thm -> term -> thm

- STRUCTURE
- SYNOPSIS
- Proves equality of equal functions applied to a term.
- DESCRIPTION
- When applied to a theorem A |- f = g and a term x, the inference rule AP_THM returns the theorem A |- f x = g x.
A |- f = g ---------------- AP_THM (A |- f = g) x A |- f x = g x

- FAILURE
- Fails unless the conclusion of the theorem is an equation, both sides of which are functions whose domain type is the same as that of the supplied term.
- SEEALSO

HOL Kananaskis-14