Tactic.ABS

ABS_TAC : tactic

SYNOPSIS

Strips lambda abstraction on both sides of an equation.

LIBRARY

bool

STRUCTURE

Tactic

DESCRIPTION

When applied to a goal of the form A ?- (\x. f x) = (\y. g u), the tactic ABS_TAC strips away the lambda abstractions:

    A ?- (\x. f x) = (\y. g y)
   ===========================  ABS_TAC
            A ?- f x = g x

FAILURE

Fails unless the goal has the above form, namely an equation both sides of which consist of a lamdba abstraction.

SEEALSO

AP_TERM_TAC, AP_THM_TAC

HOL Kananaskis-14