a generic ordering theorem used in Real

--- a/src/HOL/Ord.ML	Sat Dec 30 22:13:18 2000 +0100
+++ b/src/HOL/Ord.ML	Sat Dec 30 22:17:34 2000 +0100
@@ -48,6 +48,8 @@
 by (blast_tac (claset() addSIs [order_refl]) 1);
 qed "order_le_less";
 
+bind_thm ("order_le_imp_less_or_eq", order_le_less RS iffD1);
+
 Goal "!!x::'a::order. x < y ==> x <= y";
 by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1);
 qed "order_less_imp_le";