src/HOL/SEQ.thy
changeset 33042 ddf1f03a9ad9
parent 32960 69916a850301
child 33271 7be66dee1a5a
     1.1 --- a/src/HOL/SEQ.thy	Wed Oct 21 12:02:19 2009 +0200
     1.2 +++ b/src/HOL/SEQ.thy	Wed Oct 21 12:02:56 2009 +0200
     1.3 @@ -1089,10 +1089,10 @@
     1.4  
     1.5  subsubsection {* Cauchy Sequences are Convergent *}
     1.6  
     1.7 -axclass complete_space \<subseteq> metric_space
     1.8 -  Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X"
     1.9 +class complete_space =
    1.10 +  assumes Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X"
    1.11  
    1.12 -axclass banach \<subseteq> real_normed_vector, complete_space
    1.13 +class banach = real_normed_vector + complete_space
    1.14  
    1.15  theorem LIMSEQ_imp_Cauchy:
    1.16    assumes X: "X ----> a" shows "Cauchy X"