# 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. **)