# HG changeset patch
# User paulson
# Date 950092946 -3600
# Node ID d612354445b6fbcc9cb201975e25e614732ecc47
# Parent  a541e261c660f2974ef4b85b36bf0ebe58b74978
new thm order_less_imp_le

diff -r a541e261c660 -r d612354445b6 src/HOL/Ord.ML
--- 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)";