diff -r 3cf533397c5a -r 5fdbe2dd54f9 src/HOL/Isar_examples/Summation.thy
--- a/src/HOL/Isar_examples/Summation.thy	Sat Apr 01 20:22:46 2000 +0200
+++ b/src/HOL/Isar_examples/Summation.thy	Sat Apr 01 20:26:20 2000 +0200
@@ -47,8 +47,8 @@
   "SUM i < k. b" == "sum (\\<lambda>i. b) k";
 
 
-subsection {* Summation laws *}; (*<*)
-
+subsection {* Summation laws *};
+(*<*)
 (* FIXME binary arithmetic does not yet work here *)
 
 syntax
@@ -62,7 +62,6 @@
   "6" == "Suc (Suc 4)";
 
 theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac;
-
 (*>*)
 
 text {*