diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/abstract/Factor.thy
--- a/src/HOL/Algebra/abstract/Factor.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/abstract/Factor.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,10 +1,11 @@
-(*
-    Factorisation within a factorial domain
-    $Id$
-    Author: Clemens Ballarin, started 25 November 1997
+(*  Author: Clemens Ballarin, started 25 November 1997
+
+Factorisation within a factorial domain.
 *)
 
-theory Factor imports Ring2 begin
+theory Factor
+imports Ring2
+begin
 
 definition
   Factorisation :: "['a::ring, 'a list, 'a] => bool" where