--- a/src/HOLCF/Porder.thy Mon Jan 14 03:54:31 2008 +0100
+++ b/src/HOLCF/Porder.thy Mon Jan 14 03:56:31 2008 +0100
@@ -20,10 +20,10 @@
notation (xsymbols)
sq_le (infixl "\<sqsubseteq>" 55)
-axclass po < sq_ord
- refl_less [iff]: "x \<sqsubseteq> x"
- antisym_less: "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> x\<rbrakk> \<Longrightarrow> x = y"
- trans_less: "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
+class po = sq_ord +
+ assumes refl_less [iff]: "x \<sqsubseteq> x"
+ 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 *}