add bind_cond_pmf_cancel

add cond_map_pmf

introduce discrete conditional probabilities, use it to simplify bnf proof of pmf

tuned proof

add another lemma to split nn_integral over product count_space

tune proof

nn_integral can be split over arbitrary product count_spaces

add stronger version of lemma

default abstypes and default abstract equations make technical (no_code) annotation superfluous

careful about visibility of facts that have the same 'theory' in optimization

non-intrusive default code setup for mappings

slightly more standard code setup for String.literal, with explicit special case in predicate compiler

explicit type annotation avoids problems with Haskell type inference

more explicit hint on import order

dropped dead code; tuned

dropped obsolete external entrance point

explicit error message for non-existing targets

fixed typos

less confusing constant

tuning

simp rules for return_pmf

related permutations with bij functions

canonical name

discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;