Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
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
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
tip