isabelle: File revisions

src/HOL/Topological_Spaces.thy

Tue, 26 Mar 2013 12:20:52 +0100	hoelzl	separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef	file \| diff \| annotate
Fri, 22 Mar 2013 10:41:43 +0100	hoelzl	move continuous_on_inv to HOL image (simplifies isCont_inverse_function)	file \| diff \| annotate
Fri, 22 Mar 2013 10:41:43 +0100	hoelzl	move connected to HOL image; used to show intermediate value theorem	file \| diff \| annotate
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	file \| diff \| annotate
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)	file \| diff \| annotate
Fri, 22 Mar 2013 10:41:43 +0100	hoelzl	generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun	file \| diff \| annotate
Fri, 22 Mar 2013 10:41:43 +0100	hoelzl	move first_countable_topology to the HOL image	file \| diff \| annotate
Fri, 22 Mar 2013 10:41:42 +0100	hoelzl	move topological_space to its own theory	file \| diff \| annotate

isabelle