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.