src/HOL/Random.thy
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