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