declaring quickcheck testers as default after their setup

activating construction of exhaustive testing combinators

renamed generator into exhaustive

checking if parameter is name of a tester which allows e.g. quickcheck[random]

moving iteration of tests to the testers in quickcheck

removed dead test_term_small function in quickcheck

renamed parameter from generator to tester; quickcheck only applies one tester on invocation

adding configuration quickcheck_tester

adding smart quantifiers to exhaustive testing

adapting mutabelle

only handle TimeOut exception if used interactively

removed interrupt handling that violates Isabelle/ML exception model

corrected indentation

tuned

smallvalue_generator are defined quick via oracle or sound via function package

adding shorter output syntax for the finite types of quickcheck

improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package

changed order of lemmas to overwrite the general code equation with the nbe-specific one

adapt proofs to changed set_plus_image (cf. ee8d0548c148);

bash wrapper: terminate only in exceptional case, keep background processes running (e.g. 'thy_deps' or 'display_drafts');

updated latex dependencies (cf. 7d88ebdce380);

tuned README;

isabellesym.sty: eliminated dependency on latin1, to allow documents using utf8 instead;

proper theory name (cf. e84f82418e09);

merged;

merged

tuned cpodef code

reformulate lemma preorder.ex_ideal, and use it for typedefs

Prove rel_interior_convex_hull_union (by Grechuck Bogdan).

merged