isabelle: Graph

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

tuned signature;
2016-10-05, by wenzelm
more flexibile formatting;
2016-10-05, by wenzelm
proper calculation;
2016-10-05, by wenzelm
more operations;
2016-10-05, by wenzelm
more date and time operations from Java 8;
2016-10-05, by wenzelm
proper imports;
2016-10-05, by wenzelm
clarified modules;
2016-10-05, by wenzelm
more operations;
2016-10-05, by wenzelm
added multicore_base option;
2016-10-05, by wenzelm
allow multiple threads configurations;
2016-10-05, by wenzelm
tuned;
2016-10-05, by wenzelm
misc tuning and clarification;
2016-10-05, by wenzelm
clean output dir for fresh rebuild;
2016-10-05, by wenzelm
allow multiline script;
2016-10-05, by wenzelm
clarified sanity checks;
2016-10-05, by wenzelm
clarified modules;
2016-10-04, by wenzelm
historic workaround according to 22630327408b;
2016-10-04, by wenzelm
more thorought update of components;
2016-10-04, by wenzelm
check session name;
2016-10-04, by wenzelm
tuned signature;
2016-10-04, by wenzelm
tuned error;
2016-10-04, by wenzelm
earlier build_history_base: timing properties in log are introduced here;
2016-10-04, by wenzelm
incremental output;
2016-10-04, by wenzelm
clarified output;
2016-10-04, by wenzelm
clarified heap options;
2016-10-04, by wenzelm
proper ISABELLE_TOOL_JAVA_OPTIONS (as in "isabelle" wrapper);
2016-10-04, by wenzelm
more ambitious default as in former isatest;
2016-10-04, by wenzelm
tuned signature;
2016-10-04, by wenzelm
tuned;
2016-10-04, by wenzelm
more sanity checks;
2016-10-04, by wenzelm
more options for generated settings;
2016-10-04, by wenzelm
more robust build_history_base;
2016-10-03, by wenzelm
more robust;
2016-10-03, by wenzelm
proper log output;
2016-10-03, by wenzelm
clarified command line;
2016-10-03, by wenzelm
clarified command-line;
2016-10-03, by wenzelm
more operations;
2016-10-03, by wenzelm
more formal build_history_base;
2016-10-03, by wenzelm
clarified cold-start environment;
2016-10-03, by wenzelm
basic setup for Admin/build_history -- outside of Isabelle environment;
2016-10-03, by wenzelm
clarified: a variant of -i is the default, but its output is not as precise as it might seem;
2016-10-03, by wenzelm
merged
2016-10-05, by nipkow
replaced floorlog by floor/ceiling(log .)
2016-10-05, by nipkow
more multiset simp rules
2016-10-05, by fleury
tuned proof -- much faster
2016-10-05, by fleury
proof of concept for algebraically founded word types
2016-10-03, by haftmann
more lemmas
2016-10-03, by haftmann
option to report results of solve_direct as explicit warnings
2016-10-03, by haftmann
modernized option
2016-10-03, by haftmann
CONTRIBUTORS
2016-10-03, by haftmann
Probability: move some theorems from AFP/Density_Compiler
2016-10-03, by hoelzl
Probability: variant of central limit theorem with non-zero mean
2016-10-03, by hoelzl
HOL-Probability: more about probability, prepare for Markov processes in the AFP
2016-09-30, by hoelzl
Merge
2016-10-03, by paulson
new theorems including the theory FurtherTopology
2016-10-03, by paulson
clarified magic values (see also java/io/BufferedInputStream.java);
2016-10-03, by wenzelm
clarified stream operations;
2016-10-03, by wenzelm
tuned signature;
2016-10-03, by wenzelm
clarified modules;
2016-10-03, by wenzelm
more general read_stream: return actual byte count;
2016-10-03, by wenzelm
clarified modules;
2016-10-02, by wenzelm
more operations;
2016-10-02, by wenzelm
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