src/HOL/Enum.thy
Sat, 28 Jan 2012 12:05:26 +0100 bulwahn an executable version of accessible part (only for finite types yet)
Thu, 26 Jan 2012 12:03:35 +0100 bulwahn evaluation of THE with a non-singleton set raises a Match exception during the evaluation to yield a potential counterexample in quickcheck.
Wed, 25 Jan 2012 09:32:23 +0100 bulwahn adding code equation for Collect on finite types
Sat, 24 Dec 2011 15:53:08 +0100 haftmann enum type class instance for `set`; dropped misfitting code lemma for trancl
Fri, 14 Oct 2011 18:55:59 +0200 haftmann moved sublists to More_List.thy
Thu, 13 Oct 2011 23:35:15 +0200 haftmann avoid very specific code equation for card; corrected spelling
Thu, 13 Oct 2011 23:27:46 +0200 haftmann bouned transitive closure
Mon, 03 Oct 2011 15:39:30 +0200 bulwahn tune text for document generation
Mon, 03 Oct 2011 14:43:14 +0200 bulwahn adding code equations for cardinality and (reflexive) transitive closure on finite types
Mon, 13 Dec 2010 08:51:52 +0100 bulwahn adding an executable THE operator on finite types
Wed, 08 Dec 2010 18:07:03 +0100 bulwahn adding a smarter enumeration scheme for finite functions
Wed, 08 Dec 2010 14:25:08 +0100 bulwahn adding more efficient implementations for quantifiers in Enum
Fri, 03 Dec 2010 08:40:46 +0100 bulwahn adding shorter output syntax for the finite types of quickcheck
Fri, 03 Dec 2010 08:40:46 +0100 bulwahn changed order of lemmas to overwrite the general code equation with the nbe-specific one
Wed, 24 Nov 2010 10:52:02 +0100 bulwahn removing Enum.in_enum from the claset
Mon, 22 Nov 2010 11:35:11 +0100 bulwahn hiding enum
Mon, 22 Nov 2010 11:35:07 +0100 bulwahn hiding the constants
Mon, 22 Nov 2010 11:34:58 +0100 bulwahn adding code equations for EX1 on finite types
Mon, 22 Nov 2010 11:34:57 +0100 bulwahn adding code equation for function equality; adding some instantiations for the finite types
Mon, 22 Nov 2010 11:34:56 +0100 bulwahn adding Enum to HOL-Main image and removing it from HOL-Library
Mon, 22 Nov 2010 11:34:55 +0100 bulwahn moving Enum theory from HOL/Library to HOL
less more (0) tip