ASSUM_LIST : (thm list -> tactic) -> tactic

- STRUCTURE
- SYNOPSIS
- Applies a tactic generated from the goal’s assumption list.
- LIBRARY
- bool
- DESCRIPTION
- When applied to a function of type thm list -> tactic and a goal, ASSUM_LIST constructs a tactic by applying f to a list of ASSUMEd assumptions of the goal, then applies that tactic to the goal.
ASSUM_LIST f ({A1,...,An} ?- t) = f [A1 |- A1, ... , An |- An] ({A1,...,An} ?- t)

- FAILURE
- Fails if the function fails when applied to the list of ASSUMEd assumptions, or if the resulting tactic fails when applied to the goal.
- COMMENTS
- There is nothing magical about ASSUM_LIST: the same effect can usually be achieved just as conveniently by using ASSUME a wherever the assumption a is needed. If ASSUM_LIST is used, it is extremely unwise to use a function which selects elements from its argument list by number, since the ordering of assumptions should not be relied on.
- EXAMPLE
- The tactic:makes a single parallel substitution using all the assumptions, which can be useful if the rewriting tactics are too blunt for the required task.
ASSUM_LIST SUBST_TAC

- USES
- Making more careful use of the assumption list than simply rewriting or using resolution.
- SEEALSO

HOL Kananaskis-13