src/HOL/Enum.thy
2013-06-23 haftmann 2013-06-23 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2012-12-16 bulwahn 2012-12-16 providing a custom code equation for vimage to overwrite the vimage definition that would be rewritten by set_comprehension_pointfree simproc in the code preprocessor to an non-terminating code equation
2012-10-22 haftmann 2012-10-22 incorporated constant chars into instantiation proof for enum; tuned proofs for properties on enum of chars; swapped theory dependency of Enum.thy and String.thy
2012-10-20 haftmann 2012-10-20 tailored enum specification towards simple instantiation; tuned enum instantiations
2012-10-20 haftmann 2012-10-20 refined internal structure of Enum.thy
2012-10-20 haftmann 2012-10-20 moved quite generic material from theory Enum to more appropriate places
2012-06-25 bulwahn 2012-06-25 some special code equations for Id with class constraint enum after adding the set comprehension simproc to the code preprocessing
2012-03-30 wenzelm 2012-03-30 merged
2012-03-30 wenzelm 2012-03-30 tuned proofs, less guesswork;
2012-03-30 huffman 2012-03-30 rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'
2012-01-30 bulwahn 2012-01-30 adding code equations for max_extp and mlex
2012-01-30 bulwahn 2012-01-30 adding code equation for rtranclp in Enum
2012-01-30 bulwahn 2012-01-30 adding code equation for max_ext
2012-01-30 bulwahn 2012-01-30 adding code equation for tranclp
2012-01-28 bulwahn 2012-01-28 an executable version of accessible part (only for finite types yet)
2012-01-26 bulwahn 2012-01-26 evaluation of THE with a non-singleton set raises a Match exception during the evaluation to yield a potential counterexample in quickcheck.
2012-01-25 bulwahn 2012-01-25 adding code equation for Collect on finite types
2011-12-24 haftmann 2011-12-24 enum type class instance for `set`; dropped misfitting code lemma for trancl
2011-10-14 haftmann 2011-10-14 moved sublists to More_List.thy
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