src/HOL/Quickcheck_Random.thy
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2014-12-05 haftmann 2014-12-05 allow multiple inheritance of targets
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-09-19 blanchet 2014-09-19 made new 'primrec' bootstrapping-capable
2014-09-03 blanchet 2014-09-03 use 'datatype_new' in 'Main'
2014-01-25 haftmann 2014-01-25 prefer explicit code symbol type over ad-hoc name mangling
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