Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added order_le_less_trans, order_less_le_trans;
authorwenzelm
Fri, 04 Jun 1999 19:58:06 +0200
changeset 6780 769cea1985e4
parent 6779 2912aff958bd
child 6781 0db24da2a3c1
added order_le_less_trans, order_less_le_trans;
src/HOL/Ord.ML file | annotate | diff | comparison | revisions 
--- 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. **)
isabelle