--- 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