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;

merged

removed outdated comment moved back and updated (at the direct request of Christian Urban)

more stable introduction of the internally used unknown term

prefer typedef without alternative name;

prefer cpodef without extra definition;