MK_PABS : (thm -> thm)

- STRUCTURE
- LIBRARY
- pair
- SYNOPSIS
- Abstracts both sides of an equation.
- DESCRIPTION
- When applied to a theorem A |- !p. t1 = t2, whose conclusion is a paired universally quantified equation, MK_PABS returns the theorem A |- (\p. t1) = (\p. t2).
A |- !p. t1 = t2 -------------------------- MK_PABS A |- (\p. t1) = (\p. t2)

- FAILURE
- Fails unless the theorem is a (singly) paired universally quantified equation.
- SEEALSO

HOL Kananaskis-14