src/HOL/Library/Diagonal_Subsequence.thy
18 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
19 months ago wenzelm 2017-11-26 more symbols;
23 months ago eberlm 2017-08-17 Replaced subseq with strict_mono
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
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