isabelle: Graph

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

more operations;
2016-10-02, by wenzelm
more formal Mercurial support (with the potential to upgrade to command server);
2016-10-02, by wenzelm
tuned whitespace;
2016-10-02, by wenzelm
added isabelle_java cold-start executable;
2016-10-02, by wenzelm
updated according to 85c83757788c;
2016-10-02, by wenzelm
eliminated hard tabs;
2016-10-02, by wenzelm
updated headers;
2016-10-02, by wenzelm
updated to sumatra_pdf-3.1.2;
2016-10-02, by wenzelm
updated to xz-java-1.5;
2016-10-02, by wenzelm
updated cygwin according to 9416333a17c2, still using old 1.7.35-1;
2016-10-02, by wenzelm
tuned;
2016-10-02, by wenzelm
just one option is enough -- "isabelle jedit" java process may be prefixed directly in the shell;
2016-10-02, by wenzelm
options for process policy, notably for multiprocessor machines;
2016-10-01, by wenzelm
tuned;
2016-10-01, by wenzelm
tuned messages -- facilitate copy-paste;
2016-10-01, by wenzelm
merged
2016-10-01, by wenzelm
tuned;
2016-10-01, by wenzelm
tuned proofs;
2016-10-01, by wenzelm
Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);
2016-10-01, by wenzelm
clarified lfp/gfp statements and proofs;
2016-10-01, by wenzelm
repair LaTeX
2016-10-01, by Lars Hupel
misc tuning for release;
2016-10-01, by wenzelm
added lemma;
2016-10-01, by wenzelm
Trying out "subgoal", and no more [| |]
2016-09-30, by paulson
HOL-Analysis: fix latex generation
2016-09-30, by hoelzl
Probability: fix proof
2016-09-30, by hoelzl
Library: fix name Product_plus to Product_Plus
2016-09-30, by hoelzl
HOL-Analysis: move Product_Vector and Inner_Product from Library
2016-09-30, by hoelzl
HOL-Analysis: move Continuum_Not_Denumerable from Library
2016-09-30, by hoelzl
HOL-Analysis: move Library/Convex to Convex_Euclidean_Space
2016-09-30, by hoelzl
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
2016-09-30, by hoelzl
new material on paths, etc. Also rationalisation
2016-09-30, by paulson
Merged
2016-09-30, by Manuel Eberl
Set_Permutations replaced by more general Multiset_Permutations
2016-09-29, by eberlm
CONTRIBUTORS: new proof method "argo"
2016-09-29, by boehmes
NEWS: new proof method "argo"
2016-09-29, by boehmes
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
2016-09-29, by boehmes
invoke argo as part of the tried automatic proof methods
2016-09-29, by boehmes
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
2016-09-29, by boehmes
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
2016-09-29, by hoelzl
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
2016-09-29, by hoelzl
HOL-Analysis: move gauges and (tagged) divisions to its own theory file
2016-09-29, by hoelzl
HOL-Analysis: add cover lemma ported by L. C. Paulson
2016-09-28, by hoelzl
more new material
2016-09-29, by paulson
Generalised the type of map_poly
2016-09-29, by paulson
Merge
2016-09-28, by paulson
new material connected with HOL Light measure theory, plus more rationalisation
2016-09-28, by paulson
sequential (jobs = 1) makeall profile
2016-09-28, by Lars Hupel
syntactic type class for operation mod named after mod;
2016-09-26, by haftmann
dropped tautological pattern
2016-09-26, by haftmann
more warning comments
2016-09-26, by haftmann
more lemmas
2016-09-26, by haftmann
spelling
2016-09-26, by haftmann
a few new theorems and a renaming
2016-09-27, by paulson
use filter to define Henstock-Kurzweil integration
2016-09-26, by hoelzl
include generation time in statistics
2016-09-24, by Lars Hupel
CI script to generate timing statistics
2016-09-24, by Lars Hupel
move absolutely_integrable_on to Equivalence_Lebesgue_Henstock_Integration, now based on the Lebesgue integral
2016-09-23, by hoelzl
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
2016-09-23, by hoelzl
Merge
2016-09-22, by paulson

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip

isabelle