fix code equation for RBT_Impl.fold

merged

tail-recursive implementation for length

correct definition for skip_black

merged

merged

infprod generator works also with empty index set

add finite entropy

continuous version of mutual_information_eq_entropy_conditional_entropy

add induction for real Borel measurable functions

induction prove for positive_integral_fst

strong nonnegativ (instead of ae nn) for induction rule

induction prove for positive_integral_density

add induction rules for simple functions and for Borel measurable functions

introduce induction rules for simple functions and for Borel measurable functions

joint distribution of independent variables

indep_vars does not need sigma-sets

simplified definitions

remove unnecessary assumption from conditional_entropy_eq

alternative definition of conditional entropy

remove unneeded assumption from conditional_entropy_generic_eq

add induction rule for intersection-stable sigma-sets

show and use distributed_swap and distributed_jointI

rule to show that conditional mutual information is non-negative in the continuous case

continuous version of entropy_le

simplified entropy_uniform

remove incseq assumption from measure_eqI_generator_eq

generalize from prob_space to finite_measure

add measurable_compose

simplified assumptions for kolmogorov_0_1_law

merge should operate on pairs

remove incseq assumption from sigma_prod_algebra_sigma_eq

sigma_finite_iff_density_finite does not require a positive density function

tuned Lebesgue measure proofs

tuned product measurability

remove some unneeded positivity assumptions; generalize some assumptions to AE; tuned proofs

use continuity to show Borel-measurability

tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs

rename terminal_events to tail_event

merged

efficient construction of red black trees from sorted associative lists

more explicit code equations

adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc

special code setup for step function in IMP is redundant as definition was tuned (cf. c54d901d2946)

test case for set_comprehension_pointfree simproc succeeds now

unfolding bounded existential quantifiers as first step in the set_comprehension_pointfree simproc

moving simproc from Finite_Set to more appropriate Product_Type theory

generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)

adding some example that motivates some of the current changes in the set_comprehension_pointfree simproc

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

more consistent error messages on malformed code equations

removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands; removed '(open)', '(set_name)' and '(open set_name)' options

use Set.filter instead of Finite_Set.filter, which is removed then

rename Set.project to Set.filter - more appropriate name

added some ad-hoc namespace prefixes to avoid duplicate facts;

avoid duplicate facts;

more explicit namespace prefix for 'statespace' -- duplicate facts;

eliminated spurious fact duplicates;

modernized dynamic "rules" -- avoid rebinding of static facts;

removed redundant lemma, cf. class zero_neq_one in HOL/Rings.thy;