src/HOL/Algebra/abstract/Field.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/abstract/Field.thy	Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,15 @@
+(*
+    Properties of abstract class field
+    $Id$
+    Author: Clemens Ballarin, started 15 November 1997
+*)
+
+Field = Factor + Ideal +
+
+instance
+  field < domain (field_integral)
+
+instance
+  field < factorial (TrueI, field_fact_prime)
+
+end