src/HOL/Isar_examples/Summation.thy

   "SUM i < k. b" == "sum (%i. b) k";
 
 
 subsection {* Summation laws *};
 
-verbatim {* \begin{comment} *};
+text_raw {* \begin{comment} *};
 
 (* FIXME binary arithmetic does not yet work here *)
 
 syntax
   "3" :: nat  ("3")

   "4" == "Suc 3"
   "6" == "Suc (Suc 4)";
 
 theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac;
 
-verbatim {* \end{comment} *};
+text_raw {* \end{comment} *};
 
 
 theorem sum_of_naturals:
   "2 * (SUM i < n + 1. i) = n * (n + 1)"
   (is "?P n" is "?S n = _");