20130525 
haftmann 
20130525 
weaker precendence of syntax for big intersection and union on sets

file  diff  annotate 
20130131 
hoelzl 
20130131 
use order topology for extended reals

file  diff  annotate 
20130114 
hoelzl 
20130114 
renamed countable_basis_space to second_countable_topology

file  diff  annotate 
20121214 
wenzelm 
20121214 
updated some headers;

file  diff  annotate 
20121127 
immler 
20121127 
based countable topological basis on Countable_Set

file  diff  annotate 
20121127 
immler 
20121127 
qualified interpretation of sigma_algebra, to avoid name clashes

file  diff  annotate 
20121119 
hoelzl 
20121119 
tuned: use induction rule sigma_sets_induct_disjoint

file  diff  annotate 
20121115 
immler 
20121115 
generalized to copy of countable types instead of instantiation of nat for discrete topology

file  diff  annotate 
20121115 
immler 
20121115 
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

file  diff  annotate 