| Fri, 22 Mar 2013 10:41:43 +0100 | hoelzl | move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets | changeset | files |
| Fri, 22 Mar 2013 10:41:43 +0100 | hoelzl | move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space) | changeset | files |
| Fri, 22 Mar 2013 10:41:43 +0100 | hoelzl | clean up lemma_nest_unique and renamed to nested_sequence_unique | changeset | files |
| 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 |