MK_ABS : (thm -> thm)

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

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

HOL Kananaskis-14