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
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
do not treat interrupt as error here, to avoid confusion in log etc.;
2012-10-12, by wenzelm
more basic ML compiler messages -- avoid conflict of 638cefe3ee99 and cb7264721c91 concerning Protocol.message_positions;
2012-10-12, by wenzelm
refined separator: FBreak needs to be free for proper breaking, extra space at end helps to work around last-line oddity in jEdit;
2012-10-11, by wenzelm
merged
2012-10-11, by wenzelm
cleanup borel_measurable_positive_integral_(fst|snd)
2012-10-11, by hoelzl
msetprod based directly on Multiset.fold;
2012-10-11, by haftmann
avoid global interpretation
2012-10-11, by haftmann
simplified construction of fold combinator on multisets;
2012-10-11, by haftmann
clarified output token markup (see also bc22daeed49e);
2012-10-11, by wenzelm
refined aprop_tr' -- retain entity information by using type slot as adhoc marker;
2012-10-11, by wenzelm
refrain from quantifying outer fixes, to enable nesting of contexts like "context fixes x context assumes A x";
2012-10-11, by wenzelm
tuned;
2012-10-11, by wenzelm
tuned;
2012-10-11, by wenzelm
more position information for hyperlink and placement of message;
2012-10-11, by wenzelm
tuned;
2012-10-11, by wenzelm
mira: discontinued special settings for lxbroy10, which are probably made obsolete by newer polyml
2012-10-11, by krauss
removed unused legacy material from mira.py
2012-10-10, by krauss
eliminated some remaining uses of typedef with implicit set definition;
2012-10-10, by wenzelm
merged
2012-10-10, by Andreas Lochbihler
fix code equation for RBT_Impl.fold
2012-10-10, by Andreas Lochbihler
merged
2012-10-10, by Andreas Lochbihler
tail-recursive implementation for length
2012-10-10, by Andreas Lochbihler
correct definition for skip_black
2012-10-10, by Andreas Lochbihler
merged
2012-10-10, by wenzelm
merged
2012-10-10, by hoelzl
infprod generator works also with empty index set
2012-10-10, by hoelzl
add finite entropy
2012-10-10, by hoelzl
continuous version of mutual_information_eq_entropy_conditional_entropy
2012-10-10, by hoelzl
add induction for real Borel measurable functions
2012-10-10, by hoelzl
induction prove for positive_integral_fst
2012-10-10, by hoelzl
strong nonnegativ (instead of ae nn) for induction rule
2012-10-10, by hoelzl
induction prove for positive_integral_density
2012-10-10, by hoelzl
add induction rules for simple functions and for Borel measurable functions
2012-10-10, by hoelzl
introduce induction rules for simple functions and for Borel measurable functions
2012-10-10, by hoelzl
joint distribution of independent variables
2012-10-10, by hoelzl
indep_vars does not need sigma-sets
2012-10-10, by hoelzl
simplified definitions
2012-10-10, by hoelzl
remove unnecessary assumption from conditional_entropy_eq
2012-10-10, by hoelzl
alternative definition of conditional entropy
2012-10-10, by hoelzl
remove unneeded assumption from conditional_entropy_generic_eq
2012-10-10, by hoelzl
add induction rule for intersection-stable sigma-sets
2012-10-10, by hoelzl
show and use distributed_swap and distributed_jointI
2012-10-10, by hoelzl
rule to show that conditional mutual information is non-negative in the continuous case
2012-10-10, by hoelzl
continuous version of entropy_le
2012-10-10, by hoelzl
simplified entropy_uniform
2012-10-10, by hoelzl
remove incseq assumption from measure_eqI_generator_eq
2012-10-10, by hoelzl
generalize from prob_space to finite_measure
2012-10-10, by hoelzl
add measurable_compose
2012-10-10, by hoelzl
simplified assumptions for kolmogorov_0_1_law
2012-10-10, by hoelzl
merge should operate on pairs
2012-10-10, by hoelzl
remove incseq assumption from sigma_prod_algebra_sigma_eq
2012-10-10, by hoelzl
sigma_finite_iff_density_finite does not require a positive density function
2012-10-10, by hoelzl
tuned Lebesgue measure proofs
2012-10-10, by hoelzl
tuned product measurability
2012-10-10, by hoelzl
remove some unneeded positivity assumptions; generalize some assumptions to AE; tuned proofs
2012-10-10, by hoelzl
use continuity to show Borel-measurability
2012-10-10, by hoelzl
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
2012-10-10, by hoelzl
rename terminal_events to tail_event
2012-10-10, by hoelzl
merged
2012-10-10, by Andreas Lochbihler
efficient construction of red black trees from sorted associative lists
2012-10-10, by Andreas Lochbihler
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip