making catch_match polymorphic

compilations return genuine flag to quickcheck framework

extending quickcheck's result by the genuine flag

reporting random compilation also catches match exceptions internally

the narrowing also indicates if counterexample is potentially spurious

the simple exhaustive compilation also indicates if counterexample is potentially spurious;

quickcheck-random compilation also indicates if the counterexample is potentially spurious or not

changing the exhaustive generator signatures; replacing the hard-wired result type by its own identifier

quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception

adding examples for quickcheck-random

removing exception handling now that is caught at some other point; tuned message

quickcheck random can also find potential counterexamples; moved catch_match definition; split quickcheck setup;

merged

merged IMP/Util into IMP/Vars

use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure

cardinality of sets of lists

do not import examples Probability theory

moved theorems about distribution to the definition; removed oopsed-lemma

rename finite_prob_space.setsum_distribution, it collides with prob_space.setsum_distribution

remove duplicate theorem setsum_real_distribution

clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;

updated Sledgehammer docs with new/renamed options

added "minimize" option for more control over automatic minimization

renamed "slicing" to "slice"

tuning

minor example tweak

renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";

updated markup conforming to ML side;

discontinued obsolete datatype "alt_names";

misc tuning;