`STRIP_GOAL_THEN : thm_tactic -> tactic`

SYNOPSIS
Splits a goal by eliminating one outermost connective, applying the given theorem-tactic to the antecedents of implications.

DESCRIPTION
Given a theorem-tactic ttac and a goal (A,t), STRIP_GOAL_THEN removes one outermost occurrence of one of the connectives !, ==>, ~ or /\ from the conclusion of the goal t. If t is a universally quantified term, then STRIP_GOAL_THEN strips off the quantifier:
```      A ?- !x.u
==============  STRIP_GOAL_THEN ttac
A ?- u[x'/x]
```
where x' is a primed variant that does not appear free in the assumptions A. If t is a conjunction, then STRIP_GOAL_THEN simply splits the conjunction into two subgoals:
```      A ?- v /\ w
=================  STRIP_GOAL_THEN ttac
A ?- v   A ?- w
```
If t is an implication "u ==> v" and if:
```      A ?- v
===============  ttac (u |- u)
A' ?- v'
```
then:
```      A ?- u ==> v
====================  STRIP_GOAL_THEN ttac
A' ?- v'
```
Finally, a negation ~t is treated as the implication t ==> F.

FAILURE CONDITIONS
STRIP_GOAL_THEN ttac (A,t) fails if t is not a universally quantified term, an implication, a negation or a conjunction. Failure also occurs if the application of ttac fails, after stripping the goal.

EXAMPLE
When solving the goal
```  # g `n = 1 ==> n * n = n`;;
Warning: Free variables in goal: n
val it : goalstack = 1 subgoal (1 total)

`n = 1 ==> n * n = n`
```
a possible initial step is to apply
```  # e(STRIP_GOAL_THEN SUBST1_TAC);;
val it : goalstack = 1 subgoal (1 total)

`1 * 1 = 1`
```
which is immediate by ARITH_TAC, for example.

USES
STRIP_GOAL_THEN is used when manipulating intermediate results (obtained by stripping outer connectives from a goal) directly, rather than as assumptions.

SEE ALSO
CONJ_TAC, DISCH_THEN, GEN_TAC, STRIP_ASSUME_TAC, STRIP_TAC.