# Theory Field

Up to index of Isabelle/HOL/HOL-Algebra

theory Field
imports Factor PID
begin

    (*
        Properties of abstract class field
        $Id: Field.thy,v 1.3 2005/09/17 18:49:14 wenzelm Exp $
        Author: Clemens Ballarin, started 15 November 1997
    *)

    theory Field imports Factor PID begin

    instance field < "domain"
      apply intro_classes
       apply (rule field_one_not_zero)
      apply (erule field_integral)
      done

    instance field < factorial
      apply intro_classes
       apply (rule TrueI)
      apply (erule field_fact_prime)
      done

    end