src/HOL/Library/Order_Continuity.thy
4 months ago wenzelm 2019-03-06 removed junk;
4 months ago haftmann 2019-03-05 avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
6 months ago haftmann 2019-01-14 tuned proofs
8 months ago haftmann 2018-11-18 removed legacy input syntax
2016-10-01 wenzelm 2016-10-01 clarified lfp/gfp statements and proofs;
2016-07-22 wenzelm 2016-07-22 tuned proofs -- avoid unstructured calculation;
2016-02-19 hoelzl 2016-02-19 remove lattice syntax from countable complete lattice
2016-02-18 hoelzl 2016-02-18 add countable complete lattices
2015-11-05 wenzelm 2015-11-05 isabelle update_cartouches -c -t;
2015-07-13 hoelzl 2015-07-13 stronger induction assumption in lfp_transfer and emeasure_lfp
2015-07-03 hoelzl 2015-07-03 add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
2015-06-30 hoelzl 2015-06-30 generalized inf and sup_continuous; added intro rules
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2015-06-11 hoelzl 2015-06-11 add transfer theorems for fixed points
2015-05-04 hoelzl 2015-05-04 rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
2014-11-02 wenzelm 2014-11-02 modernized header;
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