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

extended stream library

export datatype definition which gets expanded too much in antiquotation

tuned

add induction rule for partial_function (tailrec)

prefer ownerless window, to avoid question of potentially changing parent view;

proper parent component for window.init;

lemma names and a corollary

managed to eliminate further snippets

fewer IMP snippets

merged

extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;

recovered special background handling from 8d6e478934dc, particularly relevant for gutter border;

re-init last window without flipping its visible/disposed state, to avoid odd focus inversion problems;

explicit handling of tooltip window stack -- avoid memory leak due to not-so-weak references to disposed windows (via event handlers and other aux. components);

tuned

eliminate duplicated constant (diag vs. Id_on)

hide internal constants; tuned proofs

tuned

tuned

added advanced rule induction subsection

merged

more elementary tooltips via mouse events (imitating parts of javax.swing.ToolTipManager) -- avoid abuse of getToolTipText to produce window as side-effect;

some more hammering to convince JDK 7 (and 8-ea) on Mac OS X about window size change;

more precise tooltip window size (NB: dimensions are known after layout pack, before making content visible); more precise margin width based on fractional Pretty.char_width (avoid multiplication of rounding errors); early initialization of gutter to get proper text area painter size (see also 2585c81d840a);

drop a workaround because of 8739f8abbecb

fixing transfer tactic - unfold fully identity relation by using relator_eq

tuned (in particular bold fonts)

merged

document ISABELLE_POLYML;

tuned

simplified time_CPU and time_GC; derive relative speed from time (considered as step function);

updated to scala-2.10.1;

extended stream library (sdrop_while)

tuned signature;

more robust Par_Exn.make, especially relevant for SML/NJ trying to use Par_Exn.release_all;

proper use of "member", without embarking on delicate questions about SML equality types;

made SML/NJ happy;