src/HOL/Topological_Spaces.thy
2014-08-16 wenzelm 2014-08-16 updated to named_theorems;
2014-06-30 hoelzl 2014-06-30 more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
2014-06-30 hoelzl 2014-06-30 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
2014-06-18 hoelzl 2014-06-18 filters are easier to define with INF on filters.
2014-06-18 hoelzl 2014-06-18 moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
2014-05-20 hoelzl 2014-05-20 add various lemmas
2014-05-13 hoelzl 2014-05-13 clean up Lebesgue integration
2014-04-10 kuncar 2014-04-10 setup for Transfer and Lifting from BNF; tuned thm names
2014-04-10 kuncar 2014-04-10 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
2014-04-02 hoelzl 2014-04-02 extend continuous_intros; remove continuous_on_intros and isCont_intros
2014-03-31 hoelzl 2014-03-31 add connected_local_const
2014-03-26 paulson 2014-03-26 Some useful lemmas
2014-03-20 wenzelm 2014-03-20 enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
2014-03-16 haftmann 2014-03-16 normalising simp rules for compound operators
2014-03-10 hoelzl 2014-03-10 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-03-06 blanchet 2014-03-06 renamed 'filter_rel' to 'rel_filter'
2014-03-06 blanchet 2014-03-06 renamed 'set_rel' to 'rel_set'
2014-02-27 paulson 2014-02-27 A bit of tidying up
2014-02-25 paulson 2014-02-25 More complex-related lemmas
2014-02-21 blanchet 2014-02-21 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
2014-02-18 kuncar 2014-02-18 delete or move now not necessary reflexivity rules due to 1726f46d2aa8
2014-02-12 blanchet 2014-02-12 adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
2014-02-12 blanchet 2014-02-12 renamed 'nat_{case,rec}' to '{case,rec}_nat'
2013-12-18 hoelzl 2013-12-18 modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
2013-11-05 hoelzl 2013-11-05 use bdd_above and bdd_below for conditionally complete lattices
2013-09-27 Andreas Lochbihler 2013-09-27 add relator for 'a filter and parametricity theorems
2013-09-24 huffman 2013-09-24 factor out new lemma
2013-09-24 huffman 2013-09-24 replace lemma with more general simp rule
2013-09-03 wenzelm 2013-09-03 tuned proofs -- less guessing;
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-08-27 hoelzl 2013-08-27 renamed typeclass dense_linorder to unbounded_dense_linorder
2013-07-25 haftmann 2013-07-25 factored syntactic type classes for bot and top (by Alessandro Coglio)
2013-05-30 wenzelm 2013-05-30 tuned headers;
2013-04-25 hoelzl 2013-04-25 revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
2013-04-25 hoelzl 2013-04-25 renamed linear_continuum_topology to connected_linorder_topology (and mention in NEWS)
2013-04-24 hoelzl 2013-04-24 spell conditional_ly_-complete lattices correct
2013-04-09 hoelzl 2013-04-09 remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
2013-03-26 hoelzl 2013-03-26 separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
2013-03-22 hoelzl 2013-03-22 move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
2013-03-22 hoelzl 2013-03-22 move connected to HOL image; used to show intermediate value theorem
2013-03-22 hoelzl 2013-03-22 move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets
2013-03-22 hoelzl 2013-03-22 move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
2013-03-22 hoelzl 2013-03-22 generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
2013-03-22 hoelzl 2013-03-22 move first_countable_topology to the HOL image
2013-03-22 hoelzl 2013-03-22 move topological_space to its own theory