2014-08-05 wenzelm 2014-08-05 tuned proofs;
2013-07-17 immler 2013-07-17 tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
2013-03-26 hoelzl 2013-03-26 move SEQ.thy and Lim.thy to Limits.thy
2012-11-15 immler 2012-11-15 regularity of measures, therefore: characterization of closure with infimum distance; characterize of compact sets as totally bounded; added Diagonal_Subsequence to Library; introduced (enumerable) topological basis; rational boxes as basis of ordered euclidean space; moved some lemmas upwards