[rules-dev] forall implementation by transformation?
Expert manual:
not( forall( p1 p2 p3...)) is equivalent to writing not(p1 and
not(and p2 p3...))
I think this is incorrect; it should read
forall( p1 p2 p3...) is equivalent to writing not(p1 and not(and p2 p3...))
Is this also the way forall is actually implemented?
-W