src/HOL/Isar_examples/Cantor.thy

--- a/src/HOL/Isar_examples/Cantor.thy	Mon Oct 11 20:43:38 1999 +0200
+++ b/src/HOL/Isar_examples/Cantor.thy	Mon Oct 11 20:44:23 1999 +0200
@@ -5,11 +5,8 @@
 
 header {* Cantor's Theorem *};
 
-theory Cantor = Main:;
-
-text {*
- This is an Isar'ized version of the final example of the Isabelle/HOL
- manual \cite{isabelle-HOL}.
+theory Cantor = Main:;verbatim {* \footnote{This is an Isar version of
+ the final example of the Isabelle/HOL manual \cite{isabelle-HOL}.}
 *};
 
 text {*