diff -r b2d2f1ae5808 -r e9d45709bece src/HOLCF/Porder.thy
--- 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 *}