hyp : thm -> term list
STRUCTURE
Thm
SYNOPSIS
Returns the hypotheses of a theorem.
DESCRIPTION
When applied to a theorem
A |- t
, the function
hyp
returns
A
, the list of hypotheses of the theorem.
FAILURE
Never fails.
COMMENTS
The order in which hypotheses are returned can not be relied on.
SEEALSO
dest_thm
,
concl
HOL
Kananaskis-14