src/HOL/Conditionally_Complete_Lattices.thy
Wed, 19 Mar 2014 18:47:22 +0100 haftmann elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
Sun, 16 Mar 2014 18:09:04 +0100 haftmann normalising simp rules for compound operators
Tue, 05 Nov 2013 21:23:42 +0100 hoelzl int and nat are conditionally_complete_lattices
Tue, 05 Nov 2013 09:45:02 +0100 hoelzl move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
Tue, 05 Nov 2013 09:45:00 +0100 hoelzl generalize bdd_above/below_uminus to ordered_ab_group_add
Tue, 05 Nov 2013 09:45:00 +0100 hoelzl restrict Limsup and Liminf to complete lattices
Tue, 05 Nov 2013 09:44:59 +0100 hoelzl add SUP and INF for conditionally complete lattices
Tue, 05 Nov 2013 09:44:58 +0100 hoelzl use bdd_above and bdd_below for conditionally complete lattices
Tue, 05 Nov 2013 09:44:57 +0100 hoelzl generalize SUP and INF to the syntactic type classes Sup and Inf
Tue, 27 Aug 2013 16:06:27 +0200 hoelzl renamed inner_dense_linorder to dense_linorder
Tue, 27 Aug 2013 14:37:56 +0200 hoelzl renamed typeclass dense_linorder to unbounded_dense_linorder
Thu, 30 May 2013 23:29:33 +0200 wenzelm tuned headers;
Thu, 25 Apr 2013 11:59:21 +0200 hoelzl revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
Wed, 24 Apr 2013 13:28:30 +0200 hoelzl spell conditional_ly_-complete lattices correct
less more (0) tip