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:The following application of WEAKEN_TAC does the job.
C x ------------------------------------ 0. A = B 1. B x

- 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 Kananaskis-14