src/HOL/Random.thy
Mon, 23 Jan 2012 14:00:52 +0100 bulwahn random instance for sets
Tue, 13 Sep 2011 17:07:33 -0700 huffman tuned proofs
Wed, 30 Mar 2011 11:32:52 +0200 bulwahn renewing specifications in HOL: replacing types by type_synonym
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Fri, 09 Jul 2010 08:11:10 +0200 haftmann nicer xsymbol syntax for fcomp and scomp
Thu, 29 Apr 2010 15:22:16 +0200 haftmann make random engine persistent using code_reflect
Fri, 16 Apr 2010 21:28:09 +0200 wenzelm replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
Mon, 29 Mar 2010 17:30:38 +0200 bulwahn adding values command for new monad; added new random monad compilation to predicate_compile_quickcheck
Fri, 19 Feb 2010 14:47:00 +0100 haftmann hide fact range_def
Tue, 27 Oct 2009 15:32:21 +0100 haftmann tuned
Tue, 29 Sep 2009 16:24:36 +0200 wenzelm explicit indication of Unsynchronized.ref;
Mon, 15 Jun 2009 08:16:08 +0200 haftmann where there is nothing, nothing can be hidden
Sun, 14 Jun 2009 17:20:19 +0200 haftmann dropped select_default
Wed, 27 May 2009 22:11:06 +0200 haftmann added lemma select_weight_cons_zero
Tue, 26 May 2009 17:29:33 +0200 haftmann dropped superfluos prefixes
Tue, 19 May 2009 16:54:55 +0200 haftmann String.literal replaces message_string, code_numeral replaces (code_)index
Tue, 19 May 2009 13:57:32 +0200 haftmann moved Code_Index, Random and Quickcheck before Main
Mon, 18 May 2009 15:45:42 +0200 haftmann hide fact log_def -- should not shadow regular log definition
Sat, 16 May 2009 20:16:49 +0200 haftmann experimental move of Quickcheck and related theories to HOL image
less more (0) tip