1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Algebra/abstract/Field.thy	Fri Nov 05 11:14:26 1999 +0100
     1.3 @@ -0,0 +1,15 @@
     1.4 +(*
     1.5 +    Properties of abstract class field
     1.6 +    $Id$
     1.7 +    Author: Clemens Ballarin, started 15 November 1997
     1.8 +*)
     1.9 +
    1.10 +Field = Factor + Ideal +
    1.11 +
    1.12 +instance
    1.13 +  field < domain (field_integral)
    1.14 +
    1.15 +instance
    1.16 +  field < factorial (TrueI, field_fact_prime)
    1.17 +
    1.18 +end