2013-03-26 kleing no \FIXME macro for ProgProve (moved to book)
2013-03-26 hoelzl remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
2013-03-26 hoelzl rename eventually_at / _within, to distinguish them from the lemmas in the HOL image
2013-03-26 hoelzl move theorems about compactness of real closed intervals, the intermediate value theorem, and lemmas about continuity of bijective functions from Deriv.thy to Limits.thy
2013-03-26 hoelzl Series.thy is based on Limits.thy and not Deriv.thy
2013-03-26 hoelzl move Ln.thy and Log.thy to Transcendental.thy
2013-03-26 hoelzl move SEQ.thy and Lim.thy to Limits.thy
2013-03-26 hoelzl HOL-NSA should only import Complex_Main
2013-03-26 hoelzl rename RealVector.thy to Real_Vector_Spaces.thy
2013-03-26 hoelzl rename RealDef to Real
2013-03-26 hoelzl remove Real.thy
2013-03-26 hoelzl merge RComplete into RealDef
2013-03-26 hoelzl move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings
2013-03-26 hoelzl remove posreal_complete
Loading...
(0) -30000 -10000 -3000 -1000 -300 -100 -14 +14 +100 +300 +1000 +3000 +10000 +30000 tip