src/HOL/Conditionally_Complete_Lattices.thy
Tue, 05 Nov 2013 09:44:58 +0100 use bdd_above and bdd_below for conditionally complete lattices
Tue, 05 Nov 2013 09:44:57 +0100 generalize SUP and INF to the syntactic type classes Sup and Inf
Tue, 27 Aug 2013 16:06:27 +0200 renamed inner_dense_linorder to dense_linorder
Tue, 27 Aug 2013 14:37:56 +0200 renamed typeclass dense_linorder to unbounded_dense_linorder
Thu, 30 May 2013 23:29:33 +0200 tuned headers;
Thu, 25 Apr 2013 11:59:21 +0200 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 spell conditional_ly_-complete lattices correct