--- a/src/HOL/RealDef.thy Sat May 15 16:20:54 2010 +0200
+++ b/src/HOL/RealDef.thy Sat May 15 07:48:24 2010 -0700
@@ -1055,6 +1055,7 @@
lemmas real_le_refl = order_refl [of "w::real", standard]
lemmas real_le_antisym = order_antisym [of "z::real" "w", standard]
lemmas real_le_trans = order_trans [of "i::real" "j" "k", standard]
+lemmas real_le_linear = linear [of "z::real" "w", standard]
lemmas real_le_eq_diff = le_iff_diff_le_0 [of "x::real" "y", standard]
lemmas real_add_left_mono = add_left_mono [of "x::real" "y" "z", standard]
lemmas real_mult_order = mult_pos_pos [of "x::real" "y", standard]