src/HOL/Quickcheck_Exhaustive.thy
2012-10-20 haftmann 2012-10-20 moved quite generic material from theory Enum to more appropriate places
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-03-30 bulwahn 2012-03-30 hiding fact not so aggressively
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2012-02-05 bulwahn 2012-02-05 beautifying definitions of check_all and adding instance for finite_4
2012-01-23 bulwahn 2012-01-23 random instance for sets
2012-01-20 bulwahn 2012-01-20 shortened definitions by adding some termify constants
2012-01-20 bulwahn 2012-01-20 adding check_all instance for sets; tuned
2012-01-12 bulwahn 2012-01-12 adding exhaustive instances for type constructor set
2011-12-20 bulwahn 2011-12-20 quickcheck generators for abstract types; tuned
2011-12-12 bulwahn 2011-12-12 hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
2011-12-04 bulwahn 2011-12-04 adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e); adjusting smart quickcheck compilation to new signature of exhaustive generators (cf. 1f5fc44254d7);
2011-12-01 bulwahn 2011-12-01 hiding internal constants and facts more properly
2011-12-01 bulwahn 2011-12-01 removing catch_match' now that catch_match is polymorphic
2011-12-01 bulwahn 2011-12-01 the simple exhaustive compilation also indicates if counterexample is potentially spurious;
2011-12-01 bulwahn 2011-12-01 changing the exhaustive generator signatures; replacing the hard-wired result type by its own identifier
2011-12-01 bulwahn 2011-12-01 quickcheck random can also find potential counterexamples; moved catch_match definition; split quickcheck setup;
2011-11-30 bulwahn 2011-11-30 more stable introduction of the internally used unknown term
2011-11-30 bulwahn 2011-11-30 adding a exception-safe term reification step in quickcheck; adding examples
2011-11-11 bulwahn 2011-11-11 adding CPS compilation to predicate compiler; removing function_flattening reference; new testers smart_exhaustive and smart_slow_exhaustive; renaming PredicateCompFuns to Predicate_Comp_Funs;
2011-07-18 bulwahn 2011-07-18 renaming quickcheck_tester to quickcheck_batch_tester; tuned
2011-04-08 bulwahn 2011-04-08 splitting exhaustive and full_exhaustive into separate type classes
2011-04-08 bulwahn 2011-04-08 theory definitions for fast exhaustive quickcheck compilation
2011-04-08 bulwahn 2011-04-08 new compilation for exhaustive quickcheck
2011-04-07 bulwahn 2011-04-07 removing instantiation exhaustive for unit in Quickcheck_Exhaustive
2011-04-05 bulwahn 2011-04-05 deriving bounded_forall instances in quickcheck_exhaustive
2011-04-01 bulwahn 2011-04-01 adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
2011-03-25 bulwahn 2011-03-25 changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
2011-03-11 bulwahn 2011-03-11 moving exhaustive_generators.ML to Quickcheck directory
2011-03-11 bulwahn 2011-03-11 replacing naming of small by exhaustive
2011-03-11 bulwahn 2011-03-11 renaming constants in Quickcheck_Exhaustive theory
2011-03-11 bulwahn 2011-03-11 renaming Smallcheck to Quickcheck_Exhaustive