src/HOL/Isar_examples/Cantor.thy
changeset 7869 c007f801cd59
parent 7860 7819547df4d8
child 7874 180364256231
--- a/src/HOL/Isar_examples/Cantor.thy	Thu Oct 14 15:14:14 1999 +0200
+++ b/src/HOL/Isar_examples/Cantor.thy	Thu Oct 14 16:02:39 1999 +0200
@@ -5,7 +5,7 @@
 
 header {* Cantor's Theorem *};
 
-theory Cantor = Main:;verbatim {* \footnote{This is an Isar version of
+theory Cantor = Main:;text_raw {* \footnote{This is an Isar version of
  the final example of the Isabelle/HOL manual \cite{isabelle-HOL}.}
 *};