2012-10-10 hoelzl 2012-10-10 add finite entropy
2012-10-10 hoelzl 2012-10-10 continuous version of mutual_information_eq_entropy_conditional_entropy
2012-10-10 hoelzl 2012-10-10 add induction for real Borel measurable functions
2012-10-10 hoelzl 2012-10-10 induction prove for positive_integral_fst
2012-10-10 hoelzl 2012-10-10 strong nonnegativ (instead of ae nn) for induction rule
2012-10-10 hoelzl 2012-10-10 induction prove for positive_integral_density
2012-10-10 hoelzl 2012-10-10 add induction rules for simple functions and for Borel measurable functions
2012-10-10 hoelzl 2012-10-10 introduce induction rules for simple functions and for Borel measurable functions
2012-10-10 hoelzl 2012-10-10 joint distribution of independent variables
2012-10-10 hoelzl 2012-10-10 indep_vars does not need sigma-sets
2012-10-10 hoelzl 2012-10-10 simplified definitions
2012-10-10 hoelzl 2012-10-10 remove unnecessary assumption from conditional_entropy_eq
2012-10-10 hoelzl 2012-10-10 alternative definition of conditional entropy
2012-10-10 hoelzl 2012-10-10 remove unneeded assumption from conditional_entropy_generic_eq
2012-10-10 hoelzl 2012-10-10 add induction rule for intersection-stable sigma-sets
2012-10-10 hoelzl 2012-10-10 show and use distributed_swap and distributed_jointI
2012-10-10 hoelzl 2012-10-10 rule to show that conditional mutual information is non-negative in the continuous case
2012-10-10 hoelzl 2012-10-10 continuous version of entropy_le
2012-10-10 hoelzl 2012-10-10 simplified entropy_uniform
2012-10-10 hoelzl 2012-10-10 remove incseq assumption from measure_eqI_generator_eq
2012-10-10 hoelzl 2012-10-10 generalize from prob_space to finite_measure
2012-10-10 hoelzl 2012-10-10 add measurable_compose
2012-10-10 hoelzl 2012-10-10 simplified assumptions for kolmogorov_0_1_law
2012-10-10 hoelzl 2012-10-10 merge should operate on pairs
2012-10-10 hoelzl 2012-10-10 remove incseq assumption from sigma_prod_algebra_sigma_eq
2012-10-10 hoelzl 2012-10-10 sigma_finite_iff_density_finite does not require a positive density function
2012-10-10 hoelzl 2012-10-10 tuned Lebesgue measure proofs
2012-10-10 hoelzl 2012-10-10 tuned product measurability
2012-10-10 hoelzl 2012-10-10 remove some unneeded positivity assumptions; generalize some assumptions to AE; tuned proofs
2012-10-10 hoelzl 2012-10-10 use continuity to show Borel-measurability
2012-10-10 hoelzl 2012-10-10 tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
2012-10-10 hoelzl 2012-10-10 rename terminal_events to tail_event
2012-10-10 Andreas Lochbihler 2012-10-10 merged
2012-10-10 Andreas Lochbihler 2012-10-10 efficient construction of red black trees from sorted associative lists
2012-10-10 haftmann 2012-10-10 more explicit code equations
2012-10-10 bulwahn 2012-10-10 adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
2012-10-10 bulwahn 2012-10-10 special code setup for step function in IMP is redundant as definition was tuned (cf. c54d901d2946)
2012-10-10 bulwahn 2012-10-10 test case for set_comprehension_pointfree simproc succeeds now
2012-10-10 bulwahn 2012-10-10 unfolding bounded existential quantifiers as first step in the set_comprehension_pointfree simproc
2012-10-10 bulwahn 2012-10-10 moving simproc from Finite_Set to more appropriate Product_Type theory
2012-10-10 bulwahn 2012-10-10 generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)
2012-10-10 bulwahn 2012-10-10 adding some example that motivates some of the current changes in the set_comprehension_pointfree simproc
2012-10-10 bulwahn 2012-10-10 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
2012-10-10 haftmann 2012-10-10 more consistent error messages on malformed code equations
2012-10-09 huffman 2012-10-09 removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands; removed '(open)', '(set_name)' and '(open set_name)' options
2012-10-09 kuncar 2012-10-09 use Set.filter instead of Finite_Set.filter, which is removed then
2012-10-09 kuncar 2012-10-09 rename Set.project to Set.filter - more appropriate name
2012-10-10 wenzelm 2012-10-10 added some ad-hoc namespace prefixes to avoid duplicate facts;
2012-10-10 wenzelm 2012-10-10 avoid duplicate facts;
2012-10-10 wenzelm 2012-10-10 more explicit namespace prefix for 'statespace' -- duplicate facts;
2012-10-10 wenzelm 2012-10-10 eliminated spurious fact duplicates;
2012-10-10 wenzelm 2012-10-10 modernized dynamic "rules" -- avoid rebinding of static facts;
2012-10-09 wenzelm 2012-10-09 removed redundant lemma, cf. class zero_neq_one in HOL/Rings.thy;
2012-10-09 wenzelm 2012-10-09 clarified Element.init vs. Element.activate: refrain from hard-wiring Thm.def_binding_optional to avoid duplicate facts;
2012-10-09 wenzelm 2012-10-09 tuned;
2012-10-09 wenzelm 2012-10-09 clarified Local_Defs.add_def(s): refrain from hard-wiring Thm.def_binding_optional; clarified Generic_Target.define: avoid duplicate def binding via Local_Defs.add_def;
2012-10-09 wenzelm 2012-10-09 more explicit flags for facts table;
2012-10-09 wenzelm 2012-10-09 minor tuning;
2012-10-09 wenzelm 2012-10-09 more conventional Double constants;
2012-10-09 wenzelm 2012-10-09 tuned source structure;