1\DOC AND_FORALL_CONV 2 3\TYPE {AND_FORALL_CONV : conv} 4 5\SYNOPSIS 6Moves a universal quantification outwards through a conjunction. 7 8\KEYWORDS 9conversion, quantifier. 10 11\DESCRIBE 12When applied to a term of the form {(!x.P) /\ (!x.Q)}, the conversion 13{AND_FORALL_CONV} returns the theorem: 14{ 15 |- (!x.P) /\ (!x.Q) = (!x. P /\ Q) 16} 17 18 19\FAILURE 20Fails if applied to a term not of the form {(!x.P) /\ (!x.Q)}. 21 22\COMMENTS 23It may be easier to use higher order rewriting with {FORALL_AND_THM}. 24 25\SEEALSO 26Conv.FORALL_AND_CONV, Conv.LEFT_AND_FORALL_CONV, Conv.RIGHT_AND_FORALL_CONV. 27\ENDDOC 28