src/HOL/Algebra/QuotRing.thy
changeset 27717 21bbd410ba04
parent 27611 2c01c0bdb385
child 29237 e90d9d51106b
--- a/src/HOL/Algebra/QuotRing.thy	Fri Aug 01 17:41:37 2008 +0200
+++ b/src/HOL/Algebra/QuotRing.thy	Fri Aug 01 18:10:52 2008 +0200
@@ -4,12 +4,12 @@
   Author:    Stephan Hohe
 *)
 
-header {* Quotient Rings *}
-
 theory QuotRing
 imports RingHom
 begin
 
+section {* Quotient Rings *}
+
 subsection {* Multiplication on Cosets *}
 
 constdefs (structure R)