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