Makarius

2016-01-01 21:36:02 UTC

To test the slightly updated HTML presentation in Isabelle2016-RC0 here is

an updated proof of Cantor's Theorem in HOL:

http://isabelle.in.tum.de/website-Isabelle2016-RC0/dist/library/HOL/HOL-Isar_Examples/Cantor.html

It is a return to plain reasoning, ignoring special tricks from the early

1990s to make it work "automagically".

As a proof of the elementary nature of the theorem in Higher-Order Logic,

here is also a version based on Pure + basic HOL:

http://isabelle.in.tum.de/website-Isabelle2016-RC0/dist/library/HOL/HOL-Isar_Examples/Higher_Order_Logic.html

(subsection â¹Cantor's Theoremâº). No automated reasoning tools are

available at that point. Not even the classical rule.

Technical remark: in these HTML pages the IsabelleText font is provided by

the server. So it should (in theory) work out everywhere without Unicode

dropouts. It should look exactly like in jEdit (not Isabelle/jEdit,

because the semantic markup is missing).

Makarius

an updated proof of Cantor's Theorem in HOL:

http://isabelle.in.tum.de/website-Isabelle2016-RC0/dist/library/HOL/HOL-Isar_Examples/Cantor.html

It is a return to plain reasoning, ignoring special tricks from the early

1990s to make it work "automagically".

As a proof of the elementary nature of the theorem in Higher-Order Logic,

here is also a version based on Pure + basic HOL:

http://isabelle.in.tum.de/website-Isabelle2016-RC0/dist/library/HOL/HOL-Isar_Examples/Higher_Order_Logic.html

(subsection â¹Cantor's Theoremâº). No automated reasoning tools are

available at that point. Not even the classical rule.

Technical remark: in these HTML pages the IsabelleText font is provided by

the server. So it should (in theory) work out everywhere without Unicode

dropouts. It should look exactly like in jEdit (not Isabelle/jEdit,

because the semantic markup is missing).

Makarius