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.
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
use continuity to show Borelmeasurability
20121010, by hoelzl
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
20121010, by hoelzl
rename terminal_events to tail_event
20121010, by hoelzl
merged
20121010, by Andreas Lochbihler
efficient construction of red black trees from sorted associative lists
20121010, by Andreas Lochbihler
more explicit code equations
20121010, by haftmann
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
20121010, by bulwahn
special code setup for step function in IMP is redundant as definition was tuned (cf. c54d901d2946)
20121010, by bulwahn
test case for set_comprehension_pointfree simproc succeeds now
20121010, by bulwahn
unfolding bounded existential quantifiers as first step in the set_comprehension_pointfree simproc
20121010, by bulwahn
moving simproc from Finite_Set to more appropriate Product_Type theory
20121010, by bulwahn
generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)
20121010, by bulwahn
adding some example that motivates some of the current changes in the set_comprehension_pointfree simproc
20121010, by bulwahn
set_comprehension_pointfree also handles terms where the equation is not at the first position, which is a necessary generalisation to eventually handle bounded existentials; tuned
20121010, by bulwahn
more consistent error messages on malformed code equations
20121010, by haftmann
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
20121009, by huffman
use Set.filter instead of Finite_Set.filter, which is removed then
20121009, by kuncar
rename Set.project to Set.filter  more appropriate name
20121009, by kuncar
added some adhoc namespace prefixes to avoid duplicate facts;
20121010, by wenzelm
avoid duplicate facts;
20121010, by wenzelm
more explicit namespace prefix for 'statespace'  duplicate facts;
20121010, by wenzelm
eliminated spurious fact duplicates;
20121010, by wenzelm
modernized dynamic "rules"  avoid rebinding of static facts;
20121010, by wenzelm
removed redundant lemma, cf. class zero_neq_one in HOL/Rings.thy;
20121009, by wenzelm
clarified Element.init vs. Element.activate: refrain from hardwiring Thm.def_binding_optional to avoid duplicate facts;
20121009, by wenzelm
tuned;
20121009, by wenzelm
clarified Local_Defs.add_def(s): refrain from hardwiring Thm.def_binding_optional;
20121009, by wenzelm
more explicit flags for facts table;
20121009, by wenzelm
minor tuning;
20121009, by wenzelm
more conventional Double constants;
20121009, by wenzelm
tuned source structure;
20121009, by wenzelm
tuned;
20121009, by wenzelm
tuned;
20121009, by wenzelm
less
more

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