src/HOL/Algebra/abstract/Field.thy
changeset 17479 68a7acb5f22e
parent 11093 62c2e0af1d30
child 29665 2b956243d123
     1.1 --- a/src/HOL/Algebra/abstract/Field.thy	Sat Sep 17 20:16:35 2005 +0200
     1.2 +++ b/src/HOL/Algebra/abstract/Field.thy	Sat Sep 17 20:49:14 2005 +0200
     1.3 @@ -4,12 +4,18 @@
     1.4      Author: Clemens Ballarin, started 15 November 1997
     1.5  *)
     1.6  
     1.7 -Field = Factor + PID +
     1.8 +theory Field imports Factor PID begin
     1.9  
    1.10 -instance
    1.11 -  field < domain (field_one_not_zero, field_integral)
    1.12 +instance field < "domain"
    1.13 +  apply intro_classes
    1.14 +   apply (rule field_one_not_zero)
    1.15 +  apply (erule field_integral)
    1.16 +  done
    1.17  
    1.18 -instance
    1.19 -  field < factorial (TrueI, field_fact_prime)
    1.20 +instance field < factorial
    1.21 +  apply intro_classes
    1.22 +   apply (rule TrueI)
    1.23 +  apply (erule field_fact_prime)
    1.24 +  done
    1.25  
    1.26  end