src/HOL/Algebra/abstract/Field.thy
changeset 35849 b5522b51cb1e
parent 29665 2b956243d123
--- a/src/HOL/Algebra/abstract/Field.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/abstract/Field.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,9 +1,11 @@
-(*
-    Properties of abstract class field
-    Author: Clemens Ballarin, started 15 November 1997
+(*  Author: Clemens Ballarin, started 15 November 1997
+
+Properties of abstract class field.
 *)
 
-theory Field imports Factor PID begin
+theory Field
+imports Factor PID
+begin
 
 instance field < "domain"
   apply intro_classes