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;

removed obsolete uses of ext

prefer preset = 3 -- much faster and less memory requirement;

basic support for xz files;

added component xz-java-1.2;

more "quick start" hints; more explicit "Testing of changes", instead of convoluted "Building a repository version of Isabelle"; tuned;

simple case syntax for stream (stolen from AFP/Coinductive)

prefer plain \<^sub> for better rendering (both in Isabelle/jEdit and LaTeX); tuned proofs;

merged

reverted most of 5944b20c41bf -- tends to cause race condition of synchronous vs. asynchronous version;

no censorship of "view.fracFontMetrics", although it often degrades rendering quality;

retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;

apply small result immediately, to avoid visible delay of text update after window move;

structural equality for Command.Results; more general Command.State.eq_content;

allow fractional pretty margin -- avoid premature rounding;

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); separate JEdit_Lib.pretty_metric, with slightly closer imitation of jEdit;

tuned;

spelling

fundamental revision of big operators on sets

tuned proof

locales for abstract orders

merged

added rudimentary induction rule for partial_function (heap)

allow induction predicates with arbitrary arity (not just binary)

modernized definition of root: use the_inv, handle positive and negative case uniformly, and 0-th root is constant 0

arcsin and arccos are continuous on {0 .. 1} (including the endpoints)

move continuous_on_inv to HOL image (simplifies isCont_inverse_function)

move connected to HOL image; used to show intermediate value theorem

move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets

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)

clean up lemma_nest_unique and renamed to nested_sequence_unique

simplify proof of the Bolzano bisection lemma; use more meta-logic to state it; renamed lemma_Bolzano to Bolzano

introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it

generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun

move first_countable_topology to the HOL image

move metric_space to its own theory

move topological_space to its own theory

proper metric for blanks -- NB: 70f7483df9cb discontinues coincidence of char_width with space width;

eliminated char_width_int to avoid unclear rounding; clarified integer conversion for margin;

proofs depend only on constraints, not on def of L WHILE

use the right role for SPASS hypotheses

soundness statement as in type system

add label for referencing in semantics book

tuned

get rid of xcolor warnings