src/HOL/Library/Diagonal_Subsequence.thy
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