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;

tuned

merged

clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate); clarified unknown timing vs. zero timing; tuned;

proper formatting, to facilitate line-based diff;

more uniform session descriptions, which show up in chapter index;

proper index for HOL-Proofs, which is also in chapter "HOL";

include only README.html, not historic README, which tends towards surprises like src/HOL/SPARK/Examples/README;

more accurate handling of global browser info at the very end (without races), subject to no_build and info.browser_info;

sessions may be organized via 'chapter' in ROOT;

do not absorb I/O errors;

show expanded path, to avoid odd /foo/bar/$ISABELLE_BROWSER_INFO/baz;

new lemma subset_decode_imp_le

merged

more IMP snippets

rename fset_member to fmember and prove parametricity

BNF uses fset defined via Lifting/Transfer rather than Quotient

nitpick setup and code generation for streams

merged

tuned

proper path -- I/O was hidden due to permissiveness;

merged

removed odd cvs artifacts;

refurbished some old README.html files as session descriptions, which show up in chapter index;

include session description in chapter index; prefer alphabetical order;

tuned;

more accurate theory links;

discontinued "isabelle usedir" option -r (reset session path); simplified internal session identification: chapter / name; clarified chapter index (of sessions) vs. session index (of theories); discontinued "up" links, for improved modularity also wrt. partial browser_info (users can use "back" within the browser); removed obsolete session parent_path;

discontinued "isabelle usedir" option -P (remote path);

support for 'chapter' specifications within session ROOT;

added latex markup

merged

more snippets

added pairs

extended set comprehension notation with {pttrn : A . P}

tuned

more factorisation of Step & Co

factored out Step

merged

stepwise instantiation is more modular

generalized subclass relation; tuned proof

termination proof for narrowing: fewer assumptions

accomodate encrypted file-system on linux;

tuned;

discontinued theory src/HOL/Library/Eval_Witness -- assumptions do not longer hold in presence of abstract types

updated keywords (cf. 84d01fd733cf);

proper type inference for default values

convert mappings to parametric lifting

setup_lifting doesn't support a type variable as a raw type

add [relator_mono] and [relator_distr] rules

simplify Lift_FSet because we have parametricity in Lifting now

patch Isabelle ditribution to conform to changes regarding the parametricity

lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided

merged

simplified basic termination proof

some simp rules for fset

avoid -Infinity which confuses JFreeChart histogram;

tuned proofs -- more structure, less warnings;

tuned signature -- prefer terminology of Scala and Axiom;

better message (type-unsoundnesses are becoming rare, usually the issue is elsewhere, e.g. in the TSTP proof parser)

avoid using Arith_Data.dest_sum in extended-nat simprocs (it treats 'x - y' as 'x + - y', which is not valid for enat)

netlimit is abbreviation for Lim

tuned proofs

changed has_derivative_intros into a named theorems collection

changed continuous_on_intros into a named theorems collection

changed continuous_intros into a named theorems collection

add tendsto_eq_intros: they add an additional rewriting step at the rhs of --->

major redesign: order instead of preorder, new definition of intervals as quotients

added lemma

extended numerals

merged

merged

removed unused Future.flat, while leaving its influence of Future.map (see bcd6b1aa4db5);

extended stream library a little more

extended stream library

generalized lemmas in Extended_Real_Limits

eventually nhds represented using sequentially

generalized compact_Times to topological_space

move lemma Inf to usage point

tuned proof of Edelstein fixed point theorem (use continuity of dist and attains_sup)

tuned proofs (used continuity of infdist, dist and continuous_attains_sup)

generalized continuous/compact_attains_inf/sup from real to linorder_topology

continuity of pair operations

use generate_topology for second countable topologies, does not require intersection stable basis

generalized isGlb_unique

complete_linorder is also a complete_distrib_lattice

move Liminf / Limsup lemmas on complete_lattices to its own file

merged

New theory of infinity-extended types; should replace Extended_xyz eventually

Avoid ML warning about unreferenced identifier.

polymorphic SPASS is also SPASS

allow more general coercion maps; tuned;

more lemmas about intervals

merged

refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones; refined parallel_proofs = 3: fork terminal proofs, as poor man's parallelization in interactive mode;