hoelzl [Tue, 05 Mar 2013 15:43:15 +0100] rev 52481
continuity of pair operations
hoelzl [Tue, 05 Mar 2013 15:43:14 +0100] rev 52480
use generate_topology for second countable topologies, does not require intersection stable basis
hoelzl [Tue, 05 Mar 2013 15:43:13 +0100] rev 52479
generalized isGlb_unique
hoelzl [Tue, 05 Mar 2013 15:43:12 +0100] rev 52478
complete_linorder is also a complete_distrib_lattice
hoelzl [Tue, 05 Mar 2013 15:43:08 +0100] rev 52477
move Liminf / Limsup lemmas on complete_lattices to its own file
nipkow [Tue, 05 Mar 2013 15:27:08 +0100] rev 52476
merged
nipkow [Tue, 05 Mar 2013 15:26:57 +0100] rev 52475
New theory of infinity-extended types; should replace Extended_xyz eventually
webertj [Tue, 05 Mar 2013 13:03:24 +0100] rev 52474
Avoid ML warning about unreferenced identifier.
blanchet [Tue, 05 Mar 2013 11:59:58 +0100] rev 52473
polymorphic SPASS is also SPASS
traytel [Tue, 05 Mar 2013 09:47:15 +0100] rev 52472
allow more general coercion maps; tuned;