MK_COMB_TAC : tactic

- SYNOPSIS
- Breaks an equality between applications into two equality goals: one for the functions, and other for the arguments.
- LIBRARY
- bool
- STRUCTURE
- DESCRIPTION
- MK_COMB_TAC reduces a goal of the form A ?- f x = g y to the goals A ?- f = g and A ?- x = y.
A ?- f x = g y =========================== MK_COMB_TAC A ?- f = g, A ?- x = y

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

HOL Kananaskis-14