--- a/src/HOL/Algebra/abstract/Field.thy Sat Sep 17 20:16:35 2005 +0200
+++ b/src/HOL/Algebra/abstract/Field.thy Sat Sep 17 20:49:14 2005 +0200
@@ -4,12 +4,18 @@
Author: Clemens Ballarin, started 15 November 1997
*)
-Field = Factor + PID +
+theory Field imports Factor PID begin
-instance
- field < domain (field_one_not_zero, field_integral)
+instance field < "domain"
+ apply intro_classes
+ apply (rule field_one_not_zero)
+ apply (erule field_integral)
+ done
-instance
- field < factorial (TrueI, field_fact_prime)
+instance field < factorial
+ apply intro_classes
+ apply (rule TrueI)
+ apply (erule field_fact_prime)
+ done
end