AP_TERM_TAC : tactic

- SYNOPSIS
- Strips a function application from both sides of an equational goal.
- LIBRARY
- bool
- STRUCTURE
- DESCRIPTION
- AP_TERM_TAC reduces a goal of the form A ?- f x = f y by stripping away the function applications, giving the new goal A ?- x = y.
A ?- f x = f y ================ AP_TERM_TAC A ?- x = y

- FAILURE
- Fails unless the goal is equational, with both sides being applications of the same function.
- SEEALSO

HOL Kananaskis-14