# HG changeset patch
# User haftmann
# Date 1232611486 -3600
# Node ID 1f7b1b0df292c2eaf8c304e249504d7e3dbefc74
# Parent  595d91e50510849f657340ce168cacd4720af677
simplified handling of base sort, dropped axclass

diff -r 595d91e50510 -r 1f7b1b0df292 src/HOLCF/Bifinite.thy
--- a/src/HOLCF/Bifinite.thy	Thu Jan 22 09:04:45 2009 +0100
+++ b/src/HOLCF/Bifinite.thy	Thu Jan 22 09:04:46 2009 +0100
@@ -10,7 +10,7 @@
 
 subsection {* Omega-profinite and bifinite domains *}
 
-class profinite = cpo +
+class profinite =
   fixes approx :: "nat \<Rightarrow> 'a \<rightarrow> 'a"
   assumes chain_approx [simp]: "chain approx"
   assumes lub_approx_app [simp]: "(\<Squnion>i. approx i\<cdot>x) = x"
diff -r 595d91e50510 -r 1f7b1b0df292 src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Thu Jan 22 09:04:45 2009 +0100
+++ b/src/HOLCF/Pcpo.thy	Thu Jan 22 09:04:46 2009 +0100
@@ -12,9 +12,9 @@
 
 text {* The class cpo of chain complete partial orders *}
 
-axclass cpo < po
+class cpo = po +
         -- {* class axiom: *}
-  cpo:   "chain S \<Longrightarrow> \<exists>x. range S <<| x"
+  assumes cpo:   "chain S \<Longrightarrow> \<exists>x. range S <<| x"
 
 text {* in cpo's everthing equal to THE lub has lub properties for every chain *}
 
@@ -170,8 +170,8 @@
 
 text {* The class pcpo of pointed cpos *}
 
-axclass pcpo < cpo
-  least: "\<exists>x. \<forall>y. x \<sqsubseteq> y"
+class pcpo = cpo +
+  assumes least: "\<exists>x. \<forall>y. x \<sqsubseteq> y"
 
 definition
   UU :: "'a::pcpo" where
@@ -254,13 +254,13 @@
 
 text {* further useful classes for HOLCF domains *}
 
-axclass finite_po < finite, po
+class finite_po = finite + po
 
-axclass chfin < po
-  chfin: "chain Y \<Longrightarrow> \<exists>n. max_in_chain n Y"
+class chfin = po +
+  assumes chfin: "chain Y \<Longrightarrow> \<exists>n. max_in_chain n Y"
 
-axclass flat < pcpo
-  ax_flat: "x \<sqsubseteq> y \<Longrightarrow> (x = \<bottom>) \<or> (x = y)"
+class flat = pcpo +
+  assumes ax_flat: "x \<sqsubseteq> y \<Longrightarrow> (x = \<bottom>) \<or> (x = y)"
 
 text {* finite partial orders are chain-finite *}
 
@@ -310,11 +310,11 @@
 
 text {* Discrete cpos *}
 
-axclass discrete_cpo < sq_ord
-  discrete_cpo [simp]: "x \<sqsubseteq> y \<longleftrightarrow> x = y"
+class discrete_cpo = sq_ord +
+  assumes discrete_cpo [simp]: "x \<sqsubseteq> y \<longleftrightarrow> x = y"
 
-instance discrete_cpo < po
-by (intro_classes, simp_all)
+subclass (in discrete_cpo) po
+proof qed simp_all
 
 text {* In a discrete cpo, every chain is constant *}