src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Tue Jul 27 15:39:59 2004 +0200
+++ b/src/HOL/HOL.thy	Wed Jul 28 10:49:29 2004 +0200
@@ -818,6 +818,9 @@
   apply (insert linorder_linear, blast)
   done
 
+lemma linorder_le_less_linear: "!!x::'a::linorder. x\<le>y | y<x"
+  by (simp add: order_le_less linorder_less_linear)
+
 lemma linorder_le_cases [case_names le ge]:
     "((x::'a::linorder) \<le> y ==> P) ==> (y \<le> x ==> P) ==> P"
   by (insert linorder_linear, blast)