isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 tip

NEWS;
2015-12-23, by wenzelm
tuned;
2015-12-23, by wenzelm
merged
2015-12-23, by wenzelm
tuned module arrangement;
2015-12-23, by wenzelm
tuned module arrangement;
2015-12-23, by wenzelm
check and report source at most once, notably in body of "match" method;
2015-12-23, by wenzelm
transfer rule for bounded_linear of blinfun
2015-12-23, by immler
theory for type of bounded linear functions; differentiation under the integral sign
2015-12-22, by immler
stripped some legacy
2015-12-22, by haftmann
tuned proofs and augmented some lemmas
2015-12-22, by haftmann
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
2015-12-22, by wenzelm
proper full name within the name space of the method definition;
2015-12-22, by wenzelm
tuned signature;
2015-12-22, by wenzelm
isabelle update_cartouches -c -t;
2015-12-22, by wenzelm
Merge
2015-12-22, by paulson
Liouville theorem, Fundamental Theorem of Algebra, etc.
2015-12-22, by paulson
Weierstrass: whitespace
2015-12-22, by hoelzl
merged
2015-12-22, by wenzelm
more thorough event propagation;
2015-12-22, by wenzelm
tuned -- with subtle change of order of evaluation;
2015-12-22, by wenzelm
more accurate lookup of dynamic facts;
2015-12-22, by wenzelm
tuned;
2015-12-22, by wenzelm
tuned;
2015-12-22, by wenzelm
tuned signature;
2015-12-22, by wenzelm
tuned;
2015-12-22, by wenzelm
Bochner integral: prove dominated convergence at_top
2015-12-21, by hoelzl
dead code;
2015-12-21, by wenzelm
tuned spelling;
2015-12-21, by wenzelm
merged
2015-12-21, by wenzelm
misc tuning and modernization;
2015-12-21, by wenzelm
merged
2015-12-21, by haftmann
documentation on last state of the art concerning interpretation
2015-12-19, by haftmann
abandoned attempt to unify sublocale and interpretation into global theories
2015-12-19, by haftmann
updated Cygwin (somewhere after 1.7.35-1);
2015-12-21, by wenzelm
merged
2015-12-21, by wenzelm
merged
2015-12-21, by wenzelm
tuned message;
2015-12-21, by wenzelm
more explicit ML profiling, with official Isabelle output;
2015-12-21, by wenzelm
discontinued built-in profiling: avoid danger of conflicting invocations (multithreading etc.);
2015-12-21, by wenzelm
clarified length of block with pre-existant forced breaks;
2015-12-21, by wenzelm
Probability: fix coercions (real ~> real_of_enat)
2015-12-21, by hoelzl
Transcendental: use [simp]-canonical form - (pi/2)
2015-12-21, by hoelzl
moved some theorems from the CLT proof; reordered some theorems / notation
2015-12-17, by hoelzl
tuned whitespace;
2015-12-20, by wenzelm
tuned signature;
2015-12-20, by wenzelm
renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
2015-12-20, by wenzelm
proper formatting via Pretty.string_of;
2015-12-20, by wenzelm
unused;
2015-12-20, by wenzelm
tuned;
2015-12-20, by wenzelm
prune old document versions more frequently, for reduced heap usage;
2015-12-19, by wenzelm
merged
2015-12-19, by wenzelm
more explicit Pretty.Tree, like in ML;
2015-12-19, by wenzelm
tuned;
2015-12-19, by wenzelm
clarified underlying datatypes;
2015-12-19, by wenzelm
tuned;
2015-12-19, by wenzelm
prefer default focus policy, like Output dockable;
2015-12-19, by wenzelm
tuned;
2015-12-19, by wenzelm
tuned signature;
2015-12-19, by wenzelm
support for blocks with consistent breaks;
2015-12-19, by wenzelm
preserve break indentation;
2015-12-19, by wenzelm
support pretty break indent, like underlying ML systems;
2015-12-17, by wenzelm
register record functions as 'Spec_Rules'
2015-12-19, by blanchet
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
2015-12-19, by blanchet
removed subsumed dependency
2015-12-19, by blanchet
removed dead code
2015-12-19, by blanchet
add serialisation for abs on integer to target language operation
2015-12-18, by Andreas Lochbihler
add gcd instance for integer and serialisation to target language operations
2015-12-18, by Andreas Lochbihler
merged
2015-12-16, by wenzelm
tuned whitespace;
2015-12-16, by wenzelm
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
2015-12-16, by wenzelm
tuned signature -- clarified modules;
2015-12-15, by wenzelm
unused;
2015-12-15, by wenzelm
unused;
2015-12-15, by wenzelm
Merge
2015-12-15, by paulson
New complex analysis material
2015-12-15, by paulson
infix syntax for measurable set
2015-11-25, by hoelzl
more standard term equality;
2015-12-14, by wenzelm
tuned;
2015-12-14, by wenzelm
tuned signature;
2015-12-14, by wenzelm
tuned message;
2015-12-14, by wenzelm
merged
2015-12-13, by wenzelm
more general types Proof.method / context_tactic;
2015-12-13, by wenzelm
tuned;
2015-12-12, by wenzelm
clarified ML scopes;
2015-12-12, by wenzelm
clarified ML scopes;
2015-12-12, by wenzelm
tuned;
2015-12-12, by wenzelm
unused;
2015-12-12, by wenzelm
tuned;
2015-12-12, by wenzelm
clarified modules;
2015-12-11, by wenzelm
modernized
2015-12-12, by haftmann
modernized
2015-12-12, by haftmann
modernized
2015-12-11, by haftmann
isabelle update_cartouches -c -t;
2015-12-10, by wenzelm
proper checksum for cygwin-20151210.tar.gz (some snapshot after 1.7.35-1);
2015-12-10, by wenzelm
avoid application spurious startup error;
2015-12-10, by wenzelm
current Cygwin snapshot in preparation of release;
2015-12-10, by wenzelm
hardwired LANG, to avoid sporadic surprises with local environments;
2015-12-10, by wenzelm
make SML/NJ happy;
2015-12-10, by wenzelm
not_leE -> not_le_imp_less and other tidying
2015-12-10, by paulson
clarified terminology
2015-12-07, by haftmann
tuned;
2015-12-09, by wenzelm
tuned signature;
2015-12-09, by wenzelm
tuned signature;
2015-12-09, by wenzelm
tuned;
2015-12-09, by wenzelm
more direct use of Token.src as token list;
2015-12-09, by wenzelm
merged
2015-12-09, by wenzelm
unused;
2015-12-09, by wenzelm
merged
2015-12-09, by wenzelm
clarified type Token.src: plain token list, with usual implicit value assignment;
2015-12-09, by wenzelm
tuned;
2015-12-09, by wenzelm
tuned;
2015-12-08, by wenzelm
added Proof_Context.add_thms_dynamic, which is potentially useful for Eisbach;
2015-12-08, by wenzelm
sorted out eventually_mono
2015-12-09, by paulson
tightened invariant
2015-12-08, by nipkow
isabelle update_cartouches -c -t;
2015-12-07, by wenzelm
Merge
2015-12-07, by paulson
Cauchy's integral formula for circles. Starting to fix eventually_mono.
2015-12-07, by paulson
Merged
2015-12-07, by eberlm
Generalised derivative rule for division on formal power series
2015-12-07, by eberlm
tuned;
2015-12-07, by wenzelm