`DISCH_THEN : thm_tactic -> tactic`

SYNOPSIS
Undischarges an antecedent of an implication and passes it to a theorem-tactic.

DESCRIPTION
DISCH_THEN removes the antecedent and then creates a theorem by ASSUMEing it. This new theorem is passed to the theorem-tactic given as DISCH_THEN's argument. The consequent tactic is then applied. Thus:
```   DISCH_THEN ttac (asl ?- t1 ==> t2) = ttac (ASSUME `t1`) (asl ?- t2)
```
For example, if
```    A ?- t
========  ttac (ASSUME `u`)
B ?- v
```
then
```    A ?- u ==> t
==============  DISCH_THEN ttac
B ?- v
```
Note that DISCH_THEN treats `~u` as `u ==> F`.

FAILURE CONDITIONS
DISCH_THEN will fail for goals that are not implications or negations.

EXAMPLE
Given the goal:
```  # g `!x. x = 0 ==> f(x) * x = x + 2 * x`;;
```
we can discharge the antecedent and substitute with it immediately by:
```  # e(GEN_TAC THEN DISCH_THEN SUBST1_TAC);;
val it : goalstack = 1 subgoal (1 total)

`f 0 * 0 = 0 + 2 * 0`
```
and now REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] will finish the job.