--- a/src/HOLCF/Porder.thy Wed Mar 26 22:41:58 2008 +0100
+++ b/src/HOLCF/Porder.thy Thu Mar 27 00:27:16 2008 +0100
@@ -20,10 +20,12 @@
notation (xsymbols)
sq_le (infixl "\<sqsubseteq>" 55)
-class po = sq_ord +
+class preorder = sq_ord +
assumes refl_less [iff]: "x \<sqsubseteq> x"
+ assumes trans_less: "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
+
+class po = preorder +
assumes antisym_less: "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> x\<rbrakk> \<Longrightarrow> x = y"
- assumes trans_less: "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
text {* minimal fixes least element *}