new thm order_less_imp_le

--- a/src/HOL/Ord.ML	Tue Feb 08 22:28:30 2000 +0100
+++ b/src/HOL/Ord.ML	Wed Feb 09 11:42:26 2000 +0100
@@ -48,6 +48,10 @@
 by (blast_tac (claset() addSIs [order_refl]) 1);
 qed "order_le_less";
 
+Goal "!!x::'a::order. x < y ==> x <= y";
+by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1);
+qed "order_less_imp_le";
+
 (** Asymmetry **)
 
 Goal "(x::'a::order) < y ==> ~ (y<x)";