----------------------------------------------------------------------
HALF_MK_ABS                                                 (jrhUtils)
----------------------------------------------------------------------
HALF_MK_ABS : (thm -> thm)

SYNOPSIS
Converts a function definition to lambda-form.

KEYWORDS
rule, definition.

DESCRIBE
When applied to a theorem {A |- !x. t1 x = t2}, whose conclusion is a
universally quantified equation, {HALF_MK_ABS} returns the theorem
{A |- t1 = \x. t2}.

    A |- !x. t1 x = t2
   --------------------  HALF_MK_ABS            [where x is not free in t1]
    A |- t1 = (\x. t2)




FAILURE
Fails unless the theorem is a singly universally quantified equation whose
left-hand side is a function applied to the quantified variable, or if the
variable is free in that function.

SEEALSO
Drule.ETA_CONV, Drule.MK_ABS, Thm.MK_COMB, Drule.MK_EXISTS.

----------------------------------------------------------------------