1\DOC mk_forall
2
3\TYPE {mk_forall : term * term -> term}
4
5\SYNOPSIS
6Term constructor for universal quantification.
7
8\DESCRIBE
9If {v} is a variable and {t} is a term of type {bool}, then
10{mk_forall (v,t)} returns the term {!v. t}.
11
12\FAILURE
13Fails if {v} is not a variable or if {t} is not of type {bool}.
14
15\SEEALSO
16boolSyntax.dest_forall, boolSyntax.is_forall, boolSyntax.list_mk_forall, boolSyntax.strip_forall.
17\ENDDOC
18