added axclass ordered_field;

--- a/src/HOL/Library/Ring_and_Field.thy	Fri Nov 17 18:50:52 2000 +0100
+++ b/src/HOL/Library/Ring_and_Field.thy	Sat Nov 18 00:32:08 2000 +0100
@@ -33,4 +33,9 @@
   left_inverse: "a \<noteq> 0 ==> inverse a * a = #1"
   divides_inverse: "b \<noteq> 0 ==> a / b = a * inverse b"
 
+
+axclass ordered_field < field, linorder
+  add_left_mono: "a \<le> b ==> c + a \<le> c + b"
+  mult_left_mono: "a \<le> b ==> 0 < c ==> c * a \<le> c * b"
+
 end