thm_frees : thm -> term list
- SYNOPSIS
-
Returns a list of the variables free in a theorem's assumptions and conclusion.
- DESCRIPTION
-
When applied to a theorem, A |- t, the function thm_frees returns a list,
without repetitions, of those variables which are free either in t or in
some member of the assumption list A.
- FAILURE CONDITIONS
-
Never fails.
- EXAMPLE
-
# let th = CONJUNCT1 (ASSUME `p /\ q`);;
val th : thm = p /\ q |- p
# thm_frees th;;
val it : term list = [`q`; `p`]
- SEE ALSO
-
frees, freesl, free_in.