src/HOL/Library/Order_Continuity.thy
Thu, 18 Feb 2016 13:54:44 +0100 hoelzl add countable complete lattices
Thu, 05 Nov 2015 10:39:49 +0100 wenzelm isabelle update_cartouches -c -t;
Mon, 13 Jul 2015 14:39:50 +0200 hoelzl stronger induction assumption in lfp_transfer and emeasure_lfp
Fri, 03 Jul 2015 08:26:34 +0200 hoelzl add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
Tue, 30 Jun 2015 13:30:04 +0200 hoelzl generalized inf and sup_continuous; added intro rules
Wed, 17 Jun 2015 11:03:05 +0200 wenzelm isabelle update_cartouches;
Thu, 11 Jun 2015 18:24:44 +0200 hoelzl add transfer theorems for fixed points
Mon, 04 May 2015 17:35:31 +0200 hoelzl rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
Sun, 02 Nov 2014 17:20:45 +0100 wenzelm modernized header;
Mon, 10 Mar 2014 20:04:40 +0100 hoelzl 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
less more (0) tip