# HG changeset patch
# User huffman
# Date 1273934904 25200
# Node ID fdefcbcb28878a9b21a7db07a7b5c8889359f1e4
# Parent  b4417ddad979a5dca2976b4b12d471ea7a4cb9d0
add real_le_linear to list of legacy theorem names

diff -r b4417ddad979 -r fdefcbcb2887 src/HOL/RealDef.thy
--- 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]