2013-03-22 hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51481
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
src/HOL/Deriv.thy src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy src/HOL/Multivariate_Analysis/Path_Connected.thy src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy src/HOL/RealVector.thy src/HOL/Topological_Spaces.thy src/HOL/Transcendental.thy

2013-03-22 hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51480
move connected to HOL image; used to show intermediate value theorem
src/HOL/Deriv.thy src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy src/HOL/RealVector.thy src/HOL/Topological_Spaces.thy src/HOL/ex/Gauge_Integration.thy

2013-03-22 hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51479
move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets
src/HOL/Deriv.thy src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy src/HOL/Topological_Spaces.thy

2013-03-22 hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51478
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)
src/HOL/Library/Product_Vector.thy src/HOL/Lim.thy src/HOL/Limits.thy src/HOL/Log.thy src/HOL/Metric_Spaces.thy src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy src/HOL/Multivariate_Analysis/Derivative.thy src/HOL/Multivariate_Analysis/Linear_Algebra.thy src/HOL/Multivariate_Analysis/Path_Connected.thy src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy src/HOL/NthRoot.thy src/HOL/Probability/Borel_Space.thy src/HOL/Probability/Lebesgue_Measure.thy src/HOL/Topological_Spaces.thy src/HOL/Transcendental.thy

2013-03-22 hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51477
clean up lemma_nest_unique and renamed to nested_sequence_unique
src/HOL/Deriv.thy src/HOL/SEQ.thy src/HOL/Series.thy src/HOL/Transcendental.thy

2013-03-22 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
src/HOL/Deriv.thy

2013-03-22 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
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy src/HOL/Multivariate_Analysis/Fashoda.thy src/HOL/Multivariate_Analysis/Integration.thy src/HOL/Multivariate_Analysis/Linear_Algebra.thy src/HOL/Multivariate_Analysis/Operator_Norm.thy src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy src/HOL/Probability/Probability_Measure.thy src/HOL/SupInf.thy

2013-03-22 hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51474
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
src/HOL/Limits.thy src/HOL/Metric_Spaces.thy src/HOL/NSA/HSEQ.thy src/HOL/RealVector.thy src/HOL/SEQ.thy src/HOL/Topological_Spaces.thy

2013-03-22 hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51473
move first_countable_topology to the HOL image
src/HOL/Lim.thy src/HOL/Metric_Spaces.thy src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy src/HOL/Probability/Fin_Map.thy src/HOL/Topological_Spaces.thy

2013-03-22 hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51472
move metric_space to its own theory
src/HOL/Lim.thy src/HOL/Limits.thy src/HOL/Metric_Spaces.thy src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy src/HOL/RealVector.thy src/HOL/SEQ.thy