Mercurialisabelle / file revisions
summary | shortlog | changelog | graph | tags | branches | file | revisions | annotate | diff | rss
src/HOL/Quickcheck_Exhaustive.thy
2015-02-05 haftmann 2015-02-05 slightly more standard code setup for String.literal, with explicit special case in predicate compiler file | diff | annotate
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section; file | diff | annotate
2014-10-29 wenzelm 2014-10-29 modernized setup; file | diff | annotate
2014-10-29 wenzelm 2014-10-29 tuned; file | diff | annotate
2014-09-16 blanchet 2014-09-16 added 'extraction' plugins -- this might help 'HOL-Proofs' file | diff | annotate
2014-09-14 blanchet 2014-09-14 disable datatype 'plugins' for internal types file | diff | annotate
2014-09-11 blanchet 2014-09-11 updated news file | diff | annotate
2014-09-03 blanchet 2014-09-03 use 'datatype_new' in 'Main' file | diff | annotate
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find; file | diff | annotate
2013-06-23 haftmann 2013-06-23 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier file | diff | annotate
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 file | diff | annotate
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 file | diff | annotate
2012-10-20 haftmann 2012-10-20 moved quite generic material from theory Enum to more appropriate places file | diff | annotate
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses; file | diff | annotate
2012-03-30 bulwahn 2012-03-30 hiding fact not so aggressively file | diff | annotate
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure; file | diff | annotate
2012-02-05 bulwahn 2012-02-05 beautifying definitions of check_all and adding instance for finite_4 file | diff | annotate
2012-01-23 bulwahn 2012-01-23 random instance for sets file | diff | annotate
2012-01-20 bulwahn 2012-01-20 shortened definitions by adding some termify constants file | diff | annotate
2012-01-20 bulwahn 2012-01-20 adding check_all instance for sets; tuned file | diff | annotate
2012-01-12 bulwahn 2012-01-12 adding exhaustive instances for type constructor set file | diff | annotate
2011-12-20 bulwahn 2011-12-20 quickcheck generators for abstract types; tuned file | diff | annotate
2011-12-12 bulwahn 2011-12-12 hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory; file | diff | annotate
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); file | diff | annotate
2011-12-01 bulwahn 2011-12-01 hiding internal constants and facts more properly file | diff | annotate
2011-12-01 bulwahn 2011-12-01 removing catch_match' now that catch_match is polymorphic file | diff | annotate
2011-12-01 bulwahn 2011-12-01 the simple exhaustive compilation also indicates if counterexample is potentially spurious; file | diff | annotate
2011-12-01 bulwahn 2011-12-01 changing the exhaustive generator signatures; replacing the hard-wired result type by its own identifier file | diff | annotate
2011-12-01 bulwahn 2011-12-01 quickcheck random can also find potential counterexamples; moved catch_match definition; split quickcheck setup; file | diff | annotate
2011-11-30 bulwahn 2011-11-30 more stable introduction of the internally used unknown term file | diff | annotate
2011-11-30 bulwahn 2011-11-30 adding a exception-safe term reification step in quickcheck; adding examples file | diff | annotate
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; file | diff | annotate
2011-07-18 bulwahn 2011-07-18 renaming quickcheck_tester to quickcheck_batch_tester; tuned file | diff | annotate
2011-04-08 bulwahn 2011-04-08 splitting exhaustive and full_exhaustive into separate type classes file | diff | annotate
2011-04-08 bulwahn 2011-04-08 theory definitions for fast exhaustive quickcheck compilation file | diff | annotate
2011-04-08 bulwahn 2011-04-08 new compilation for exhaustive quickcheck file | diff | annotate
2011-04-07 bulwahn 2011-04-07 removing instantiation exhaustive for unit in Quickcheck_Exhaustive file | diff | annotate
2011-04-05 bulwahn 2011-04-05 deriving bounded_forall instances in quickcheck_exhaustive file | diff | annotate
2011-04-01 bulwahn 2011-04-01 adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall file | diff | annotate
2011-03-25 bulwahn 2011-03-25 changing iteration scheme of functions to use minimal number of function updates for exhaustive testing file | diff | annotate
2011-03-11 bulwahn 2011-03-11 moving exhaustive_generators.ML to Quickcheck directory file | diff | annotate
2011-03-11 bulwahn 2011-03-11 replacing naming of small by exhaustive file | diff | annotate
2011-03-11 bulwahn 2011-03-11 renaming constants in Quickcheck_Exhaustive theory file | diff | annotate
2011-03-11 bulwahn 2011-03-11 renaming Smallcheck to Quickcheck_Exhaustive file | diff | annotate | base
isabelle