src/HOL/Enum.thy
2010-12-13 bulwahn 2010-12-13 adding an executable THE operator on finite types
2010-12-08 bulwahn 2010-12-08 adding a smarter enumeration scheme for finite functions
2010-12-08 bulwahn 2010-12-08 adding more efficient implementations for quantifiers in Enum
2010-12-03 bulwahn 2010-12-03 adding shorter output syntax for the finite types of quickcheck
2010-12-03 bulwahn 2010-12-03 changed order of lemmas to overwrite the general code equation with the nbe-specific one
2010-11-24 bulwahn 2010-11-24 removing Enum.in_enum from the claset
2010-11-22 bulwahn 2010-11-22 hiding enum
2010-11-22 bulwahn 2010-11-22 hiding the constants
2010-11-22 bulwahn 2010-11-22 adding code equations for EX1 on finite types
2010-11-22 bulwahn 2010-11-22 adding code equation for function equality; adding some instantiations for the finite types
2010-11-22 bulwahn 2010-11-22 adding Enum to HOL-Main image and removing it from HOL-Library
2010-11-22 bulwahn 2010-11-22 moving Enum theory from HOL/Library to HOL