--- a/src/HOLCF/Porder.thy Wed Jun 18 23:03:11 2008 +0200
+++ b/src/HOLCF/Porder.thy Wed Jun 18 23:07:30 2008 +0200
@@ -20,11 +20,9 @@
notation (xsymbols)
sq_le (infixl "\<sqsubseteq>" 55)
-class preorder = sq_ord +
+class po = 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"
text {* minimal fixes least element *}