src/HOL/Enum.thy
2014-10-10 haftmann 2014-10-10 specialized specification: avoid trivial instances
2014-09-16 blanchet 2014-09-16 added 'extraction' plugins -- this might help 'HOL-Proofs'
2014-09-14 blanchet 2014-09-14 disable datatype 'plugins' for internal types
2014-09-11 blanchet 2014-09-11 updated news
2014-09-03 blanchet 2014-09-03 use 'datatype_new' in 'Main'
2014-08-31 haftmann 2014-08-31 separated listsum material
2014-08-13 Andreas Lochbihler 2014-08-13 add algebraic type class instances for Enum.finite* types
2014-08-08 Andreas Lochbihler 2014-08-08 add complete_lattice instances for Enum.finite_* types such that quickcheck deals with lattice class operations
2014-06-12 nipkow 2014-06-12 added [simp]
2014-01-20 blanchet 2014-01-20 moved 'bacc' back to 'Enum' (cf. 744934b818c7) -- reduces baggage loaded by 'Hilbert_Choice'
2014-01-01 haftmann 2014-01-01 fundamental treatment of undefined vs. universally partial replaces code_abort
2013-11-10 haftmann 2013-11-10 qualifed popular user space names
2013-10-18 blanchet 2013-10-18 killed more "no_atp"s
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
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