20140412 
nipkow 
20140412 
made mult_pos_pos a simp rule

file  diff  annotate 
20140411 
nipkow 
20140411 
made divide_pos_pos a simp rule

file  diff  annotate 
20140318 
haftmann 
20140318 
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly

file  diff  annotate 
20140318 
hoelzl 
20140318 
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}

file  diff  annotate 
20140316 
haftmann 
20140316 
normalising simp rules for compound operators

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