On 16 Nov 2011, at 15:17, Phil Clayton wrote:
I suspect those involved with large scale theorem proving will start moving to 64 bit OSes, if not already, so one application can address more than 4GB memory, as that amount of physical memory is becoming quite common these days.
Seconded: at least one user of ProofPower (me) and many users of Isabelle are already in that situation.
Regards,
Rob.