src/HOL/Isar_examples/Cantor.thy
 changeset 7800 8ee919e42174 parent 7748 5b9c45b21782 child 7819 6dd018b6cf3f
--- a/src/HOL/Isar_examples/Cantor.thy	Fri Oct 08 15:08:47 1999 +0200
+++ b/src/HOL/Isar_examples/Cantor.thy	Fri Oct 08 15:09:14 1999 +0200
@@ -6,15 +6,16 @@
chapter of "Isabelle's Object-Logics" (Larry Paulson).
*)

-header {* More classical proofs: Cantor's Theorem *};

theory Cantor = Main:;

text {*
Cantor's Theorem states that every set has more subsets than it has
-  elements.  It has become a favourite basic example in higher-order logic
-  since it is so easily expressed: $\all{f::\alpha \To \alpha \To \idt{bool}} - \ex{S::\alpha \To \idt{bool}} \all{x::\alpha}. f \ap x \not= S$
+  elements.  It has become a favorite basic example in pure
+  higher-order logic since it is so easily expressed: $\all{f::\alpha + \To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}} + \all{x::\alpha}. f \ap x \not= S$

Viewing types as sets, $\alpha \To \idt{bool}$ represents the powerset of
$\alpha$.  This version of the theorem states that for every function from