diff -r 37a92211a5d3 -r dbb95b825244 src/HOL/Algebra/CRing.thy
--- a/src/HOL/Algebra/CRing.thy	Fri Apr 16 04:06:52 2004 +0200
+++ b/src/HOL/Algebra/CRing.thy	Fri Apr 16 04:07:10 2004 +0200
@@ -5,11 +5,11 @@
   Copyright: Clemens Ballarin
 *)
 
+header {* Abelian Groups *}
+
 theory CRing = FiniteProduct
 files ("ringsimp.ML"):
 
-section {* Abelian Groups *}
-
 record 'a ring = "'a monoid" +
   zero :: 'a ("\<zero>\<index>")
   add :: "['a, 'a] => 'a" (infixl "\<oplus>\<index>" 65)