ANTS_TAC : tactic

SYNOPSIS

Split off antecedent of antecedent of goal as a new subgoal.

DESCRIPTION

   A ?- (p ==> q) ==> r
  ======================= ANTS_TAC
   A ?- p   A ?- q ==> r

FAILURE CONDITIONS

Fails unless the goal is of the specified form.

USES

Convenient for focusing on assumptions of an implicational theorem that one wants to use.

SEE ALSO

MP_TAC.