# HG changeset patch
# User huffman
# Date 1200279391 -3600
# Node ID e9d45709bece3c8f0a134bd3831c2457cbde73cc
# Parent  b2d2f1ae5808766866b65885bdcec0dc5995a6dd
use new-style class for po

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 *}
 
diff -r b2d2f1ae5808 -r e9d45709bece src/HOLCF/SetPcpo.thy
--- a/src/HOLCF/SetPcpo.thy	Mon Jan 14 03:54:31 2008 +0100
+++ b/src/HOLCF/SetPcpo.thy	Mon Jan 14 03:56:31 2008 +0100
@@ -9,17 +9,16 @@
 imports Adm
 begin
 
-instantiation set :: (type) sq_ord
+instantiation set :: (type) po
 begin
 
 definition
   less_set_def: "(op \<sqsubseteq>) = (op \<subseteq>)"
 
-instance ..
-end
+instance
+by (intro_classes, auto simp add: less_set_def)
 
-instance set :: (type) po
-by (intro_classes, auto simp add: less_set_def)
+end
 
 instance set :: (finite) finite_po ..