# HG changeset patch
# User paulson
# Date 978211054 -3600
# Node ID e43e017df8c1a2827dfdd34ab1328d019b414a1b
# Parent  c4f1bf2acf4ccdcbaabf0b45025c41c8c7ec458c
a generic ordering theorem used in Real

diff -r c4f1bf2acf4c -r e43e017df8c1 src/HOL/Ord.ML
--- 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";