generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
no_document use_thys ["~~/src/HOL/Library/While_Combinator"];
use_thys ["MicroJava"];