find_termHolKernel.find_term : (term -> bool) -> term -> termFinds a sub-term satisfying a predicate.
A call to find_term P t returns a sub-term of
t that satisfies the predicate P if there is
one. Otherwise it raises a HOL_ERR exception. The search is
done in a top-down, left-to-right order (i.e., rators of combs are
examined before rands).
Fails if the predicate fails when applied to any of the sub-terms of the term argument. Also fails if there is no sub-term satisfying the predicate.
- find_term Literal.is_numeral ``2 + x + 3``;
> val it = ``2`` : term
- find_term Literal.is_numeral ``x + y``;
Exception HOL_ERR {...}