src/HOL/Quickcheck_Exhaustive.thy
2017-05-29 eberlm 2017-05-29 reorganised material on sublists
2016-12-23 haftmann 2016-12-23 restored instance for char, which got ancidentally lost in b3f2b8c906a6
2016-04-14 wenzelm 2016-04-14 misc tuning and standardization;
2016-03-12 haftmann 2016-03-12 model characters directly as range 0..255 * * * operate on syntax terms rather than asts
2016-02-18 haftmann 2016-02-18 more direct bootstrap of char type, still retaining the nibble representation for syntax
2015-09-06 wenzelm 2015-09-06 do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-02-05 haftmann 2015-02-05 slightly more standard code setup for String.literal, with explicit special case in predicate compiler
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-10-29 wenzelm 2014-10-29 tuned;
2014-09-16 blanchet 2014-09-16 added 'extraction' plugins -- this might help 'HOL-Proofs'
2014-09-14 blanchet 2014-09-14 disable datatype 'plugins' for internal types
2014-09-11 blanchet 2014-09-11 updated news
2014-09-03 blanchet 2014-09-03 use 'datatype_new' in 'Main'
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-06-23 haftmann 2013-06-23 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2013-02-15 haftmann 2013-02-15 two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one
2013-02-14 haftmann 2013-02-14 reform of predicate compiler / quickcheck theories: implement yieldn operations uniformly on the ML level -- predicate compiler uses negative integers as parameter to yieldn, whereas code_numeral represents natural numbers! avoid odd New_ prefix by joining related theories; avoid overcompact name DSequence; separated predicate inside random monad into separate theory; consolidated name of theory Quickcheck
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