equal
deleted
inserted
replaced
3 Author: Markus Wenzel, TU Muenchen |
3 Author: Markus Wenzel, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header {* Cantor's Theorem *}; |
6 header {* Cantor's Theorem *}; |
7 |
7 |
8 theory Cantor = Main:; |
8 theory Cantor = Main:;verbatim {* \footnote{This is an Isar version of |
9 |
9 the final example of the Isabelle/HOL manual \cite{isabelle-HOL}.} |
10 text {* |
|
11 This is an Isar'ized version of the final example of the Isabelle/HOL |
|
12 manual \cite{isabelle-HOL}. |
|
13 *}; |
10 *}; |
14 |
11 |
15 text {* |
12 text {* |
16 Cantor's Theorem states that every set has more subsets than it has |
13 Cantor's Theorem states that every set has more subsets than it has |
17 elements. It has become a favorite basic example in pure |
14 elements. It has become a favorite basic example in pure |