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