src/HOL/Random.thy
Thu, 12 Nov 2020 09:06:44 +0100 haftmann bundled syntax for state monad combinators
Wed, 06 Jun 2018 11:12:37 +0200 nipkow Keep filter input syntax
Tue, 22 May 2018 11:08:37 +0200 nipkow First step to remove nonstandard "[x <- xs. P]" syntax: only input
Thu, 15 Sep 2016 11:48:20 +0200 nipkow renamed listsum -> sum_list, listprod ~> prod_list
Sun, 13 Mar 2016 10:22:46 +0100 haftmann more theorems on orderings
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Sun, 31 Aug 2014 09:10:42 +0200 haftmann separated listsum material
Thu, 12 Jun 2014 17:02:03 +0200 blanchet tuned dependencies
Thu, 12 Jun 2014 01:00:49 +0200 blanchet register record extensions as freely generated types
Fri, 15 Feb 2013 08:31:31 +0100 haftmann two target language numeral types: integer and natural, as replacement for code_numeral;
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