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