[isabelle] Proving Cantor's Theorem


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.


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