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 JavaScriptenabled browsers.
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
300
100
60
+60
+100
+300
+1000
+3000
+10000
tip