2011-10-13 haftmann 2011-10-13 avoid very specific code equation for card; corrected spelling
2011-10-13 haftmann 2011-10-13 bouned transitive closure
2011-10-03 bulwahn 2011-10-03 tune text for document generation
2011-10-03 bulwahn 2011-10-03 adding code equations for cardinality and (reflexive) transitive closure on finite types
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