simplified construction of fold combinator on multisets; more coherent name for fold combinator on multisets

clarified output token markup (see also bc22daeed49e);

refined aprop_tr' -- retain entity information by using type slot as adhoc marker;

refrain from quantifying outer fixes, to enable nesting of contexts like "context fixes x context assumes A x"; tuned;

tuned;

tuned;

more position information for hyperlink and placement of message;

tuned;

mira: discontinued special settings for lxbroy10, which are probably made obsolete by newer polyml

removed unused legacy material from mira.py

eliminated some remaining uses of typedef with implicit set definition;

merged

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)