PRED_ASSUM : (term -> bool) -> thm_tactic -> tactic

- STRUCTURE
- SYNOPSIS
- Discharges a selected assumption and passes it to a theorem-tactic.
- DESCRIPTION
- PRED_ASSUM finds the first assumption satisfying the prediate given, removes it from the assumption list, ASSUMEs it, passes it to the theorem-tactic and then applies the consequent tactic. Thus, where t is the first assumption satisfying p,For example (again, where t is the first assumption in A u {t} satisfying p), if
PRED_ASSUM p f ([a1,... ai, t, aj, ... an], goal) = f (ASSUME t) ([a1,... ai, aj,... an], goal)

thenA ?- c ======== f (ASSUME t) B ?- v

A u {t} ?- c =============== PRED_ASSUM p f B ?- v

- FAILURE
- PRED_ASSUM p will fail on goals where no assumption safisfies p.
- SEEALSO

HOL Kananaskis-13