# HG changeset patch
# User haftmann
# Date 1244124663 -7200
# Node ID d1cb222438d852e6e577d2e6589313b02c69ebc8
# Parent  55edadbd43d585951f2cd0d206c9af4906dff14e
class replaces axclass

diff -r 55edadbd43d5 -r d1cb222438d8 src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Thu Jun 04 15:28:59 2009 +0200
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Thu Jun 04 16:11:03 2009 +0200
@@ -484,25 +484,30 @@
 
 subsection{* Hausdorff and other separation properties *}
 
-axclass t0_space \<subseteq> topological_space
-  t0_space:
-    "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U)"
-
-axclass t1_space \<subseteq> topological_space
-  t1_space:
-    "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<notin> U \<and> x \<notin> V \<and> y \<in> V"
-
-instance t1_space \<subseteq> t0_space
-by default (fast dest: t1_space)
+class t0_space =
+  assumes t0_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U)"
+
+class t1_space =
+  assumes t1_space: "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<notin> U \<and> x \<notin> V \<and> y \<in> V"
+begin
+
+subclass t0_space
+proof
+qed (fast dest: t1_space)
+
+end
 
 text {* T2 spaces are also known as Hausdorff spaces. *}
 
-axclass t2_space \<subseteq> topological_space
-  hausdorff:
-    "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
-
-instance t2_space \<subseteq> t1_space
-by default (fast dest: hausdorff)
+class t2_space =
+  assumes hausdorff: "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
+begin
+
+subclass t1_space
+proof
+qed (fast dest: hausdorff)
+
+end
 
 instance metric_space \<subseteq> t2_space
 proof
@@ -568,9 +573,9 @@
   using approachable_lt_le[where f="\<lambda>x'. dist x' x" and P="\<lambda>x'. \<not> (x'\<in>S \<and> x'\<noteq>x)"]
   by metis (* FIXME: VERY slow! *)
 
-axclass perfect_space \<subseteq> metric_space
+class perfect_space =
   (* FIXME: perfect_space should inherit from topological_space *)
-  islimpt_UNIV [simp, intro]: "x islimpt UNIV"
+  assumes islimpt_UNIV [simp, intro]: "(x::'a::metric_space) islimpt UNIV"
 
 lemma perfect_choose_dist:
   fixes x :: "'a::perfect_space"