src/HOL/Library/Liminf_Limsup.thy
2015-12-17 hoelzl 2015-12-17 moved some theorems from the CLT proof; reordered some theorems / notation
2015-12-09 paulson 2015-12-09 sorted out eventually_mono
2015-12-07 paulson 2015-12-07 Cauchy's integral formula for circles. Starting to fix eventually_mono.
2015-11-21 wenzelm 2015-11-21 tuned proofs;
2015-11-05 wenzelm 2015-11-05 isabelle update_cartouches -c -t;
2015-09-25 hoelzl 2015-09-25 prove Liminf_inverse_ereal
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
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-18 haftmann 2014-03-18 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
2013-11-05 hoelzl 2013-11-05 restrict Limsup and Liminf to complete lattices
2013-11-05 hoelzl 2013-11-05 generalize SUP and INF to the syntactic type classes Sup and Inf
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 inner_dense_linorder to dense_linorder
2013-03-26 wenzelm 2013-03-26 tuned imports;
2013-03-05 hoelzl 2013-03-05 move Liminf / Limsup lemmas on complete_lattices to its own file