Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Proving Cantor's Theorem

Email Gateway (Aug 18 2022 at 20:14):

From: John Munroe <munddr@gmail.com>
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

Last updated: Apr 20 2024 at 04:19 UTC