WEAKEN_TAC : (term -> bool) -> tactic
STRUCTURE
SYNOPSIS
Deletes assumption from goal.
DESCRIPTION
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
HOL  Trindemossen-1