src/HOL/Algebra/abstract/Field.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 11093 62c2e0af1d30
child 17479 68a7acb5f22e
permissions -rw-r--r--
Constant "If" is now local
paulson@7998
     1
(*
paulson@7998
     2
    Properties of abstract class field
paulson@7998
     3
    $Id$
paulson@7998
     4
    Author: Clemens Ballarin, started 15 November 1997
paulson@7998
     5
*)
paulson@7998
     6
ballarin@11093
     7
Field = Factor + PID +
paulson@7998
     8
paulson@7998
     9
instance
ballarin@11093
    10
  field < domain (field_one_not_zero, field_integral)
paulson@7998
    11
paulson@7998
    12
instance
paulson@7998
    13
  field < factorial (TrueI, field_fact_prime)
paulson@7998
    14
paulson@7998
    15
end