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