| Fri, 22 Mar 2013 10:41:43 +0100 | hoelzl | introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it | changeset | files |
| Fri, 22 Mar 2013 10:41:43 +0100 | hoelzl | generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun | changeset | files |
| Fri, 22 Mar 2013 10:41:43 +0100 | hoelzl | move first_countable_topology to the HOL image | changeset | files |
| Fri, 22 Mar 2013 10:41:43 +0100 | hoelzl | move metric_space to its own theory | changeset | files |