2015-12-23 ago wenzelm NEWS;
2015-12-23 ago wenzelm tuned;
2015-12-23 ago wenzelm merged
2015-12-23 ago wenzelm tuned module arrangement;
2015-12-23 ago wenzelm tuned module arrangement;
2015-12-23 ago wenzelm check and report source at most once, notably in body of "match" method;
2015-12-23 ago immler transfer rule for bounded_linear of blinfun
2015-12-22 ago immler theory for type of bounded linear functions; differentiation under the integral sign
2015-12-22 ago haftmann stripped some legacy
2015-12-22 ago haftmann tuned proofs and augmented some lemmas
2015-12-22 ago wenzelm more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
2015-12-22 ago wenzelm proper full name within the name space of the method definition;
2015-12-22 ago wenzelm tuned signature;
2015-12-22 ago wenzelm isabelle update_cartouches -c -t;
2015-12-22 ago paulson Merge
2015-12-22 ago paulson Liouville theorem, Fundamental Theorem of Algebra, etc.
2015-12-22 ago hoelzl Weierstrass: whitespace
2015-12-22 ago wenzelm merged
2015-12-22 ago wenzelm more thorough event propagation;
2015-12-22 ago wenzelm tuned -- with subtle change of order of evaluation;
2015-12-22 ago wenzelm more accurate lookup of dynamic facts;
2015-12-22 ago wenzelm tuned;
2015-12-22 ago wenzelm tuned;
2015-12-22 ago wenzelm tuned signature;
2015-12-22 ago wenzelm tuned;
2015-12-21 ago hoelzl Bochner integral: prove dominated convergence at_top
2015-12-21 ago wenzelm dead code;
2015-12-21 ago wenzelm tuned spelling;
2015-12-21 ago wenzelm merged
2015-12-21 ago wenzelm misc tuning and modernization;
2015-12-21 ago haftmann merged
2015-12-21 ago wenzelm updated Cygwin (somewhere after 1.7.35-1);
2015-12-21 ago wenzelm merged
2015-12-21 ago wenzelm merged
2015-12-21 ago wenzelm tuned message;
2015-12-21 ago wenzelm more explicit ML profiling, with official Isabelle output;
2015-12-21 ago wenzelm discontinued built-in profiling: avoid danger of conflicting invocations (multithreading etc.);
2015-12-21 ago wenzelm clarified length of block with pre-existant forced breaks;
2015-12-21 ago hoelzl Probability: fix coercions (real ~> real_of_enat)
2015-12-21 ago hoelzl Transcendental: use [simp]-canonical form - (pi/2)
2015-12-17 ago hoelzl moved some theorems from the CLT proof; reordered some theorems / notation
2015-12-20 ago wenzelm tuned whitespace;
2015-12-20 ago wenzelm tuned signature;
2015-12-20 ago wenzelm renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
2015-12-20 ago wenzelm proper formatting via Pretty.string_of;
2015-12-20 ago wenzelm unused;
2015-12-20 ago wenzelm tuned;
2015-12-19 ago wenzelm prune old document versions more frequently, for reduced heap usage;
2015-12-19 ago wenzelm merged
2015-12-19 ago wenzelm more explicit Pretty.Tree, like in ML;
2015-12-19 ago wenzelm tuned;
2015-12-19 ago wenzelm clarified underlying datatypes;
2015-12-19 ago wenzelm tuned;
2015-12-19 ago wenzelm prefer default focus policy, like Output dockable;
2015-12-19 ago wenzelm tuned;
2015-12-19 ago wenzelm tuned signature;
2015-12-19 ago wenzelm support for blocks with consistent breaks;
2015-12-19 ago wenzelm preserve break indentation;
2015-12-17 ago wenzelm support pretty break indent, like underlying ML systems;
2015-12-19 ago blanchet register record functions as 'Spec_Rules'