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
2013-03-26 hoelzl separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
2013-03-25 ballarin Discontinued theories src/HOL/Algebra/abstract and .../poly.
2013-03-25 ballarin Remove obsolete URLs in documentation of HOL-Algebra.
2013-03-25 ballarin Fix issue related to mixins in roundup.
2013-03-25 kleing simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
2013-03-25 nipkow added lemmas
2013-03-25 wenzelm merged
2013-03-25 wenzelm clarified text_fold vs. fbrk;
2013-03-25 wenzelm tuned print_classes: more standard order, markup, formatting;
2013-03-25 wenzelm tuned message;
2013-03-25 wenzelm actually exit on scalac failure;
2013-03-25 wenzelm tuned signature;
2013-03-25 kleing removed obsolete uses of ext
2013-03-24 wenzelm prefer preset = 3 -- much faster and less memory requirement;
2013-03-24 wenzelm basic support for xz files;
2013-03-24 wenzelm added component xz-java-1.2;
2013-03-24 wenzelm more "quick start" hints;
2013-03-24 traytel simple case syntax for stream (stolen from AFP/Coinductive)
2013-03-23 wenzelm prefer plain \<^sub> for better rendering (both in Isabelle/jEdit and LaTeX);
2013-03-23 wenzelm merged
2013-03-23 wenzelm reverted most of 5944b20c41bf -- tends to cause race condition of synchronous vs. asynchronous version;
2013-03-23 wenzelm no censorship of "view.fracFontMetrics", although it often degrades rendering quality;
2013-03-23 wenzelm retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
2013-03-23 wenzelm apply small result immediately, to avoid visible delay of text update after window move;
2013-03-23 wenzelm structural equality for Command.Results;
2013-03-23 wenzelm allow fractional pretty margin -- avoid premature rounding;
2013-03-23 wenzelm more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
2013-03-23 wenzelm tuned;
2013-03-23 haftmann spelling
2013-03-23 haftmann fundamental revision of big operators on sets
2013-03-23 haftmann tuned proof
2013-03-23 haftmann locales for abstract orders
2013-03-23 krauss merged
2013-03-21 krauss added rudimentary induction rule for partial_function (heap)
2013-03-21 krauss allow induction predicates with arbitrary arity (not just binary)
2013-03-22 hoelzl modernized definition of root: use the_inv, handle positive and negative case uniformly, and 0-th root is constant 0
2013-03-22 hoelzl arcsin and arccos are continuous on {0 .. 1} (including the endpoints)
2013-03-22 hoelzl move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
2013-03-22 hoelzl move connected to HOL image; used to show intermediate value theorem
2013-03-22 hoelzl move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets
2013-03-22 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)
2013-03-22 hoelzl clean up lemma_nest_unique and renamed to nested_sequence_unique
2013-03-22 hoelzl simplify proof of the Bolzano bisection lemma; use more meta-logic to state it; renamed lemma_Bolzano to Bolzano
2013-03-22 hoelzl introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
2013-03-22 hoelzl generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
2013-03-22 hoelzl move first_countable_topology to the HOL image
2013-03-22 hoelzl move metric_space to its own theory
2013-03-22 hoelzl move topological_space to its own theory
2013-03-21 wenzelm proper metric for blanks -- NB: 70f7483df9cb discontinues coincidence of char_width with space width;
2013-03-21 wenzelm eliminated char_width_int to avoid unclear rounding;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip