Mercurial
Mercurial
>
repos
>
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
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScriptenabled browsers.
more sanity checks;
20161004, by wenzelm
more options for generated settings;
20161004, by wenzelm
more robust build_history_base;
20161003, by wenzelm
more robust;
20161003, by wenzelm
proper log output;
20161003, by wenzelm
clarified command line;
20161003, by wenzelm
clarified commandline;
20161003, by wenzelm
more operations;
20161003, by wenzelm
more formal build_history_base;
20161003, by wenzelm
clarified coldstart environment;
20161003, by wenzelm
basic setup for Admin/build_history  outside of Isabelle environment;
20161003, by wenzelm
clarified: a variant of i is the default, but its output is not as precise as it might seem;
20161003, by wenzelm
merged
20161005, by nipkow
replaced floorlog by floor/ceiling(log .)
20161005, by nipkow
more multiset simp rules
20161005, by fleury
tuned proof  much faster
20161005, by fleury
proof of concept for algebraically founded word types
20161003, by haftmann
more lemmas
20161003, by haftmann
option to report results of solve_direct as explicit warnings
20161003, by haftmann
modernized option
20161003, by haftmann
CONTRIBUTORS
20161003, by haftmann
Probability: move some theorems from AFP/Density_Compiler
20161003, by hoelzl
Probability: variant of central limit theorem with nonzero mean
20161003, by hoelzl
HOLProbability: more about probability, prepare for Markov processes in the AFP
20160930, by hoelzl
Merge
20161003, by paulson
new theorems including the theory FurtherTopology
20161003, by paulson
clarified magic values (see also java/io/BufferedInputStream.java);
20161003, by wenzelm
clarified stream operations;
20161003, by wenzelm
tuned signature;
20161003, by wenzelm
clarified modules;
20161003, by wenzelm
more general read_stream: return actual byte count;
20161003, by wenzelm
clarified modules;
20161002, by wenzelm
more operations;
20161002, by wenzelm
more operations;
20161002, by wenzelm
more formal Mercurial support (with the potential to upgrade to command server);
20161002, by wenzelm
tuned whitespace;
20161002, by wenzelm
added isabelle_java coldstart executable;
20161002, by wenzelm
updated according to 85c83757788c;
20161002, by wenzelm
eliminated hard tabs;
20161002, by wenzelm
updated headers;
20161002, by wenzelm
updated to sumatra_pdf3.1.2;
20161002, by wenzelm
updated to xzjava1.5;
20161002, by wenzelm
updated cygwin according to 9416333a17c2, still using old 1.7.351;
20161002, by wenzelm
tuned;
20161002, by wenzelm
just one option is enough  "isabelle jedit" java process may be prefixed directly in the shell;
20161002, by wenzelm
options for process policy, notably for multiprocessor machines;
20161001, by wenzelm
tuned;
20161001, by wenzelm
tuned messages  facilitate copypaste;
20161001, by wenzelm
merged
20161001, by wenzelm
tuned;
20161001, by wenzelm
tuned proofs;
20161001, by wenzelm
Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);
20161001, by wenzelm
clarified lfp/gfp statements and proofs;
20161001, by wenzelm
repair LaTeX
20161001, by Lars Hupel
misc tuning for release;
20161001, by wenzelm
added lemma;
20161001, by wenzelm
Trying out "subgoal", and no more [ ]
20160930, by paulson
HOLAnalysis: fix latex generation
20160930, by hoelzl
Probability: fix proof
20160930, by hoelzl
Library: fix name Product_plus to Product_Plus
20160930, by hoelzl
HOLAnalysis: move Product_Vector and Inner_Product from Library
20160930, by hoelzl
HOLAnalysis: move Continuum_Not_Denumerable from Library
20160930, by hoelzl
HOLAnalysis: move Library/Convex to Convex_Euclidean_Space
20160930, by hoelzl
HOLAnalysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
20160930, by hoelzl
new material on paths, etc. Also rationalisation
20160930, by paulson
Merged
20160930, by Manuel Eberl
Set_Permutations replaced by more general Multiset_Permutations
20160929, by eberlm
CONTRIBUTORS: new proof method "argo"
20160929, by boehmes
NEWS: new proof method "argo"
20160929, by boehmes
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
20160929, by boehmes
invoke argo as part of the tried automatic proof methods
20160929, by boehmes
new proof method "argo" for a combination of quantifierfree propositional logic with equality and linear real arithmetic
20160929, by boehmes
HOLAnalysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
20160929, by hoelzl
HOLAnalysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
20160929, by hoelzl
HOLAnalysis: move gauges and (tagged) divisions to its own theory file
20160929, by hoelzl
HOLAnalysis: add cover lemma ported by L. C. Paulson
20160928, by hoelzl
more new material
20160929, by paulson
Generalised the type of map_poly
20160929, by paulson
Merge
20160928, by paulson
new material connected with HOL Light measure theory, plus more rationalisation
20160928, by paulson
sequential (jobs = 1) makeall profile
20160928, by Lars Hupel
syntactic type class for operation mod named after mod;
20160926, by haftmann
dropped tautological pattern
20160926, by haftmann
more warning comments
20160926, by haftmann
more lemmas
20160926, by haftmann
spelling
20160926, by haftmann
a few new theorems and a renaming
20160927, by paulson
use filter to define HenstockKurzweil integration
20160926, by hoelzl
include generation time in statistics
20160924, by Lars Hupel
CI script to generate timing statistics
20160924, by Lars Hupel
move absolutely_integrable_on to Equivalence_Lebesgue_Henstock_Integration, now based on the Lebesgue integral
20160923, by hoelzl
prove HKintegrable implies Lebesgue measurable; prove HKintegral equals Lebesgue integral for nonneg functions
20160923, by hoelzl
Merge
20160922, by paulson
More mainly topological results
20160922, by paulson
merged
20160922, by wenzelm
discontinued raw symbols;
20160922, by wenzelm
raw control symbols are superseded by Latex.embed_raw;
20160922, by wenzelm
\<^raw> output is intended for LaTeX;
20160921, by wenzelm
more general mixfix delimiters;
20160921, by wenzelm
more tight implementation of symbol explode operation (without support for raw symbols);
20160921, by wenzelm
approximation: preprocessing for nat/int expressions
20160921, by immler
provide more information on error
20160921, by immler
approximation: rewrite for reduction to base expressions
20160921, by immler
new material about topological concepts, etc
20160921, by paulson
vector_add_divide_simps now a "named theorems" bundle
20160921, by paulson
tuned  fewer warnings;
20160920, by wenzelm
avoid old SML90;
20160920, by wenzelm
more generic algebraic lemmas
20160918, by haftmann
NEWS: Normalized_Fraction.thy
20160920, by eberlm
Merged
20160920, by eberlm
Additions to permutations (contributed by Lukas Bulwahn)
20160919, by eberlm
resolve the name clash of HOL/Library/FSet and HOL/Quotient_Examples/FSet
20160919, by kuncar
# after multiset intersection and union symbol
20160919, by fleury
left_distrib ~> distrib_right, right_distrib ~> distrib_left
20160919, by fleury
tuned;
20160919, by wenzelm
merged
20160918, by wenzelm
tuned proofs;
20160918, by wenzelm
merged
20160918, by Lars Hupel
tuned
20160918, by Lars Hupel
clarified notation: iterated quantifier is negated as one chunk;
20160918, by wenzelm
less
more

(0)
30000
10000
3000
1000
120
+120
+1000
+3000
+10000
tip