2017-04-12 haftmann 2017-04-12 tuned
2016-07-22 wenzelm 2016-07-22 tuned proofs -- avoid unstructured calculation;
2016-06-17 hoelzl 2016-06-17 move Conditional_Complete_Lattices to Main
2016-05-27 wenzelm 2016-05-27 tuned proofs;
2016-05-13 wenzelm 2016-05-13 eliminated use of empty "assms";
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-03-16 paulson 2016-03-16 Contractible sets. Also removal of obsolete theorems and refactoring
2016-02-22 paulson 2016-02-22 An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
2016-02-17 haftmann 2016-02-17 prefer abbreviations for compound operators INFIMUM and SUPREMUM
2015-12-10 paulson 2015-12-10 not_leE -> not_le_imp_less and other tidying
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-06-30 paulson 2015-06-30 Useful lemmas. The theorem concerning swapping the variables in a double integral.
2015-05-04 hoelzl 2015-05-04 rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
2015-01-27 hoelzl 2015-01-27 ereal: tuned proofs concerning continuity and suprema
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
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 moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
2014-03-19 haftmann 2014-03-19 elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
2014-03-16 haftmann 2014-03-16 normalising simp rules for compound operators
2013-11-05 hoelzl 2013-11-05 int and nat are conditionally_complete_lattices
2013-11-05 hoelzl 2013-11-05 move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
2013-11-05 hoelzl 2013-11-05 generalize bdd_above/below_uminus to ordered_ab_group_add
2013-11-05 hoelzl 2013-11-05 restrict Limsup and Liminf to complete lattices
2013-11-05 hoelzl 2013-11-05 add SUP and INF for conditionally complete lattices
2013-11-05 hoelzl 2013-11-05 use bdd_above and bdd_below for conditionally complete lattices
2013-11-05 hoelzl 2013-11-05 generalize SUP and INF to the syntactic type classes Sup and Inf
2013-08-27 hoelzl 2013-08-27 renamed inner_dense_linorder to dense_linorder
2013-08-27 hoelzl 2013-08-27 renamed typeclass dense_linorder to unbounded_dense_linorder
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-24 hoelzl 2013-04-24 spell conditional_ly_-complete lattices correct