[isabelle] Proving Cantor's Theorem



Hi,

Would it be right to say that the automation of the proof of Cantor's
Theorem is one of the earliest significant achievements of
higher-order unification?

If not, is there a more profound, better example?

Thanks in advance.

John





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.