AP_THM_TAC : tactic

- SYNOPSIS
- Strips identical operands from functions on both sides of an equation.
- LIBRARY
- bool
- STRUCTURE
- DESCRIPTION
- When applied to a goal of the form A ?- f x = g x, the tactic AP_THM_TAC strips away the operands of the function application:
A ?- f x = g x ================ AP_THM_TAC A ?- f = g

- FAILURE
- Fails unless the goal has the above form, namely an equation both sides of which consist of function applications to the same arguments.
- SEEALSO

HOL Kananaskis-14