src/HOL/Isar_examples/Summation.thy

--- a/src/HOL/Isar_examples/Summation.thy	Thu Oct 14 15:14:14 1999 +0200
+++ b/src/HOL/Isar_examples/Summation.thy	Thu Oct 14 16:02:39 1999 +0200
@@ -30,7 +30,7 @@
 
 subsection {* Summation laws *};
 
-verbatim {* \begin{comment} *};
+text_raw {* \begin{comment} *};
 
 (* FIXME binary arithmetic does not yet work here *)
 
@@ -46,7 +46,7 @@
 
 theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac;
 
-verbatim {* \end{comment} *};
+text_raw {* \end{comment} *};
 
 
 theorem sum_of_naturals: