# [isabelle] Cantor's Theorem

`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

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