| Fri, 22 Mar 2013 10:41:43 +0100 | hoelzl | simplify proof of the Bolzano bisection lemma; use more meta-logic to state it; renamed lemma_Bolzano to Bolzano | changeset | files |
| 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 |
| Fri, 22 Mar 2013 10:41:42 +0100 | hoelzl | move topological_space to its own theory | changeset | files |
| Thu, 21 Mar 2013 16:58:14 +0100 | wenzelm | proper metric for blanks -- NB: 70f7483df9cb discontinues coincidence of char_width with space width; | changeset | files |