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.
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
tuned proofs;
20160918, by wenzelm
tuned;
20160918, by wenzelm
clarified notation;
20160918, by wenzelm
support replicate_mset in multiset simproc
20160918, by fleury
tuning multiset simproc
20160918, by fleury
repair LaTeX dropout from f83ef97d8d7d
20160917, by Lars Hupel
prefer abbreviation for trivial set conversion
20160916, by haftmann
more lemmas
20160916, by haftmann
merged
20160916, by wenzelm
more symbols  as in the printed document;
20160916, by wenzelm
more symbols;
20160916, by wenzelm
tuned proofs
20160916, by Lars Hupel
misc updates;
20160916, by wenzelm
merged
20160916, by wenzelm
consolidate implicit use of gnutar, via somewhat fragile dynamic scoping within existing shell scripts;
20160916, by wenzelm
merged
20160916, by immler
Liminf/Limsup and filtermap
20160915, by immler
less
more

(0)
30000
10000
3000
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
tip