tuned whitespace;

eliminated some legacy operations;

removed dead code, which has never been active in recorded history;

do not open ML structures;

tuned signature;

hide quickcheck constants Abs_cfun and Rep_cfun, to avoid clash with HOLCF

hiding internal constants and facts more properly

removing catch_match' now that catch_match is polymorphic

adapting exhaustive generators in record package

outputing if counterexample is potentially spurious or not

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