diff -r 3246e66b0874 -r e25eedfc15ce src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Wed Feb 10 08:49:26 2010 +0100
+++ b/src/HOL/Fields.thy	Wed Feb 10 08:49:26 2010 +0100
@@ -14,8 +14,8 @@
 begin
 
 class field = comm_ring_1 + inverse +
-  assumes field_inverse:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
-  assumes divide_inverse: "a / b = a * inverse b"
+  assumes field_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
+  assumes field_divide_inverse: "a / b = a * inverse b"
 begin
 
 subclass division_ring
@@ -24,6 +24,9 @@
   assume "a \<noteq> 0"
   thus "inverse a * a = 1" by (rule field_inverse)
   thus "a * inverse a = 1" by (simp only: mult_commute)
+next
+  fix a b :: 'a
+  show "a / b = a * inverse b" by (rule field_divide_inverse)
 qed
 
 subclass idom ..