rename eventually_at / _within, to distinguish them from the lemmas in the HOL image

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

Series.thy is based on Limits.thy and not Deriv.thy

move Ln.thy and Log.thy to Transcendental.thy

move SEQ.thy and Lim.thy to Limits.thy

HOL-NSA should only import Complex_Main

rename RealVector.thy to Real_Vector_Spaces.thy

rename RealDef to Real

remove Real.thy

merge RComplete into RealDef

move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings

remove posreal_complete

separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef

Discontinued theories src/HOL/Algebra/abstract and .../poly.

Remove obsolete URLs in documentation of HOL-Algebra.

Fix issue related to mixins in roundup. Previously, mixins were only applied one level down the DFS tree while they should also be applied at the level of declaration. Makes the algorithm consistent with the version presented in the upcoming JAR paper.

simp_const -> afold; bfold -> fold'; bsimp_const -> bfold

added lemmas

merged

clarified text_fold vs. fbrk;

tuned print_classes: more standard order, markup, formatting; uniform printing of minimal supersort/classrel;

tuned message;

actually exit on scalac failure;

tuned signature;