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