# HG changeset patch
# User huffman
# Date 1136945404 -3600
# Node ID 5f5d37e763c49131b05e7d90326eedc59889b7e2
# Parent  612dcdd9c03dc8b2e8f4565de40a6e4909face33
add transitivity rules

diff -r 612dcdd9c03d -r 5f5d37e763c4 src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Wed Jan 11 00:11:05 2006 +0100
+++ b/src/HOLCF/Porder.thy	Wed Jan 11 03:10:04 2006 +0100
@@ -46,6 +46,18 @@
 lemma rev_trans_less: "\<lbrakk>(y::'a::po) \<sqsubseteq> z; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
 by (rule trans_less)
 
+lemma sq_ord_less_eq_trans: "\<lbrakk>a \<sqsubseteq> b; b = c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
+by (rule subst)
+
+lemma sq_ord_eq_less_trans: "\<lbrakk>a = b; b \<sqsubseteq> c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
+by (rule ssubst)
+
+lemmas HOLCF_trans_rules [trans] =
+  trans_less
+  antisym_less
+  sq_ord_less_eq_trans
+  sq_ord_eq_less_trans
+
 subsection {* Chains and least upper bounds *}
 
 constdefs