----------------------------------------------------------------------
WEAKEN_TAC                                                    (Tactic)
----------------------------------------------------------------------
WEAKEN_TAC : (term -> bool) -> tactic

SYNOPSIS
Deletes assumption from goal.

KEYWORDS
tactic, assumption.

DESCRIBE
Given an ML predicate {P} mapping terms to {true} or {false} and
a goal {(asl,g)}, an invocation {WEAKEN_TAC P (asl,g)} removes the
first element (call it {tm}) that {P} holds of from {asl}, returning
the goal {(asl - tm,g)}.

FAILURE
Fails if the assumption list of the goal is empty, or if {P} holds
of no element in {asl}.

EXAMPLE
Suppose we want to dispose of the equality assumption in
the following goal:

    C x
    ------------------------------------
      0.  A = B
      1.  B x

The following application of {WEAKEN_TAC} does the job.

  - e (WEAKEN_TAC is_eq);
  OK..
  1 subgoal:
  > val it =
      C x
      ------------------------------------
        B x




USES
Occasionally useful for getting rid of superfluous assumptions.



SEEALSO
Tactical.PAT_ASSUM, Tactical.POP_ASSUM.

----------------------------------------------------------------------