src/HOL/Random.thy
2014-08-31 haftmann 2014-08-31 separated listsum material
2014-06-12 blanchet 2014-06-12 tuned dependencies
2014-06-12 blanchet 2014-06-12 register record extensions as freely generated types
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
2012-01-23 bulwahn 2012-01-23 random instance for sets
2011-09-13 huffman 2011-09-13 tuned proofs
2011-03-30 bulwahn 2011-03-30 renewing specifications in HOL: replacing types by type_synonym
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-07-09 haftmann 2010-07-09 nicer xsymbol syntax for fcomp and scomp
2010-04-29 haftmann 2010-04-29 make random engine persistent using code_reflect
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-03-29 bulwahn 2010-03-29 adding values command for new monad; added new random monad compilation to predicate_compile_quickcheck
2010-02-19 haftmann 2010-02-19 hide fact range_def
2009-10-27 haftmann 2009-10-27 tuned
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-06-15 haftmann 2009-06-15 where there is nothing, nothing can be hidden
2009-06-14 haftmann 2009-06-14 dropped select_default
2009-05-27 haftmann 2009-05-27 added lemma select_weight_cons_zero
2009-05-26 haftmann 2009-05-26 dropped superfluos prefixes
2009-05-19 haftmann 2009-05-19 String.literal replaces message_string, code_numeral replaces (code_)index
2009-05-19 haftmann 2009-05-19 moved Code_Index, Random and Quickcheck before Main
2009-05-18 haftmann 2009-05-18 hide fact log_def -- should not shadow regular log definition
2009-05-16 haftmann 2009-05-16 experimental move of Quickcheck and related theories to HOL image