src/HOL/Fields.thy

--- a/src/HOL/Fields.thy	Tue Apr 27 08:18:25 2010 +0200
+++ b/src/HOL/Fields.thy	Tue Apr 27 09:49:36 2010 +0200
@@ -643,13 +643,9 @@
 
 end
 
-class linordered_field_inverse_zero = linordered_field +
-  assumes linordered_field_inverse_zero: "inverse 0 = 0"
+class linordered_field_inverse_zero = linordered_field + field_inverse_zero
 begin
 
-subclass field_inverse_zero proof
-qed (fact linordered_field_inverse_zero)
-
 lemma le_divide_eq:
   "(a \<le> b/c) = 
    (if 0 < c then a*c \<le> b