src/HOL/Conditionally_Complete_Lattices.thy
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