--- a/src/HOL/SEQ.thy Wed Oct 21 12:02:19 2009 +0200
+++ b/src/HOL/SEQ.thy Wed Oct 21 12:02:56 2009 +0200
@@ -1089,10 +1089,10 @@
subsubsection {* Cauchy Sequences are Convergent *}
-axclass complete_space \<subseteq> metric_space
- Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X"
+class complete_space =
+ assumes Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X"
-axclass banach \<subseteq> real_normed_vector, complete_space
+class banach = real_normed_vector + complete_space
theorem LIMSEQ_imp_Cauchy:
assumes X: "X ----> a" shows "Cauchy X"