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.
discontinued obsolete typedef (open) syntax;
20121012, by wenzelm
discontinued typedef with implicit set_def;
20121012, by wenzelm
merged
20121012, by wenzelm
increading indexes to avoid clashes in the set_comprehension_pointfree simproc
20121012, by bulwahn
no special treatment of errors inside goal forks without transaction id, to avoid duplication in plain build with sequential log, for example;
20121012, by wenzelm
do not treat interrupt as error here, to avoid confusion in log etc.;
20121012, by wenzelm
more basic ML compiler messages  avoid conflict of 638cefe3ee99 and cb7264721c91 concerning Protocol.message_positions;
20121012, by wenzelm
refined separator: FBreak needs to be free for proper breaking, extra space at end helps to work around lastline oddity in jEdit;
20121011, by wenzelm
merged
20121011, by wenzelm
cleanup borel_measurable_positive_integral_(fstsnd)
20121011, by hoelzl
msetprod based directly on Multiset.fold;
20121011, by haftmann
avoid global interpretation
20121011, by haftmann
simplified construction of fold combinator on multisets;
20121011, by haftmann
clarified output token markup (see also bc22daeed49e);
20121011, by wenzelm
refined aprop_tr'  retain entity information by using type slot as adhoc marker;
20121011, by wenzelm
refrain from quantifying outer fixes, to enable nesting of contexts like "context fixes x context assumes A x";
20121011, by wenzelm
tuned;
20121011, by wenzelm
tuned;
20121011, by wenzelm
more position information for hyperlink and placement of message;
20121011, by wenzelm
tuned;
20121011, by wenzelm
mira: discontinued special settings for lxbroy10, which are probably made obsolete by newer polyml
20121011, by krauss
removed unused legacy material from mira.py
20121010, by krauss
eliminated some remaining uses of typedef with implicit set definition;
20121010, by wenzelm
merged
20121010, by Andreas Lochbihler
fix code equation for RBT_Impl.fold
20121010, by Andreas Lochbihler
merged
20121010, by Andreas Lochbihler
tailrecursive implementation for length
20121010, by Andreas Lochbihler
correct definition for skip_black
20121010, by Andreas Lochbihler
merged
20121010, by wenzelm
merged
20121010, by hoelzl
infprod generator works also with empty index set
20121010, by hoelzl
add finite entropy
20121010, by hoelzl
continuous version of mutual_information_eq_entropy_conditional_entropy
20121010, by hoelzl
add induction for real Borel measurable functions
20121010, by hoelzl
induction prove for positive_integral_fst
20121010, by hoelzl
strong nonnegativ (instead of ae nn) for induction rule
20121010, by hoelzl
induction prove for positive_integral_density
20121010, by hoelzl
add induction rules for simple functions and for Borel measurable functions
20121010, by hoelzl
introduce induction rules for simple functions and for Borel measurable functions
20121010, by hoelzl
joint distribution of independent variables
20121010, by hoelzl
indep_vars does not need sigmasets
20121010, by hoelzl
simplified definitions
20121010, by hoelzl
remove unnecessary assumption from conditional_entropy_eq
20121010, by hoelzl
alternative definition of conditional entropy
20121010, by hoelzl
remove unneeded assumption from conditional_entropy_generic_eq
20121010, by hoelzl
add induction rule for intersectionstable sigmasets
20121010, by hoelzl
show and use distributed_swap and distributed_jointI
20121010, by hoelzl
rule to show that conditional mutual information is nonnegative in the continuous case
20121010, by hoelzl
continuous version of entropy_le
20121010, by hoelzl
simplified entropy_uniform
20121010, by hoelzl
remove incseq assumption from measure_eqI_generator_eq
20121010, by hoelzl
generalize from prob_space to finite_measure
20121010, by hoelzl
add measurable_compose
20121010, by hoelzl
simplified assumptions for kolmogorov_0_1_law
20121010, by hoelzl
merge should operate on pairs
20121010, by hoelzl
remove incseq assumption from sigma_prod_algebra_sigma_eq
20121010, by hoelzl
sigma_finite_iff_density_finite does not require a positive density function
20121010, by hoelzl
tuned Lebesgue measure proofs
20121010, by hoelzl
tuned product measurability
20121010, by hoelzl
remove some unneeded positivity assumptions; generalize some assumptions to AE; tuned proofs
20121010, by hoelzl
less
more

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