# HG changeset patch
# User wenzelm
# Date 928519086 -7200
# Node ID 769cea1985e466142b674fa63097811e9d6883cc
# Parent  2912aff958bda07c80872a4db9a8dfd98d89a09f
added order_le_less_trans, order_less_le_trans;

diff -r 2912aff958bd -r 769cea1985e4 src/HOL/Ord.ML
--- a/src/HOL/Ord.ML	Fri Jun 04 19:57:31 1999 +0200
+++ b/src/HOL/Ord.ML	Fri Jun 04 19:58:06 1999 +0200
@@ -62,6 +62,16 @@
 by (blast_tac (claset() addIs [order_trans,order_antisym]) 1);
 qed "order_less_trans";
 
+Goal "!!x::'a::order. [| x <= y; y < z |] ==> x < z";
+by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1);
+by (blast_tac (claset() addIs [order_trans,order_antisym]) 1);
+qed "order_le_less_trans";
+
+Goal "!!x::'a::order. [| x < y; y <= z |] ==> x < z";
+by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1);
+by (blast_tac (claset() addIs [order_trans,order_antisym]) 1);
+qed "order_less_le_trans";
+
 
 (** Useful for simplification, but too risky to include by default. **)