Fri, 22 Mar 2013 10:41:43 +0100 clean up lemma_nest_unique and renamed to nested_sequence_unique
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51477
clean up lemma_nest_unique and renamed to nested_sequence_unique
Fri, 22 Mar 2013 10:41:43 +0100 simplify proof of the Bolzano bisection lemma; use more meta-logic to state it; renamed lemma_Bolzano to Bolzano
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51476
simplify proof of the Bolzano bisection lemma; use more meta-logic to state it; renamed lemma_Bolzano to Bolzano
Fri, 22 Mar 2013 10:41:43 +0100 introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51475
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
Fri, 22 Mar 2013 10:41:43 +0100 generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51474
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
Fri, 22 Mar 2013 10:41:43 +0100 move first_countable_topology to the HOL image
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51473
move first_countable_topology to the HOL image
Fri, 22 Mar 2013 10:41:43 +0100 move metric_space to its own theory
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51472
move metric_space to its own theory
Fri, 22 Mar 2013 10:41:42 +0100 move topological_space to its own theory
hoelzl [Fri, 22 Mar 2013 10:41:42 +0100] rev 51471
move topological_space to its own theory
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -7 +7 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip