src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
2013-02-15 haftmann 2013-02-15 two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one
2012-08-01 wenzelm 2012-08-01 fixed document;
2012-04-30 bulwahn 2012-04-30 removing obsolete setup for sets now that sets are executable
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-03-13 wenzelm 2012-03-13 prefer abs_def over def_raw;
2012-03-12 noschinl 2012-03-12 tuned proofs
2011-12-24 haftmann 2011-12-24 adjusted to set/pred distinction by means of type constructor `set`
2011-11-11 bulwahn 2011-11-11 using more conventional names for monad plus operations
2011-10-21 bulwahn 2011-10-21 replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
2011-09-14 hoelzl 2011-09-14 renamed Complete_Lattices lemmas, removed legacy names
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-08-17 wenzelm 2011-08-17 modernized signature of Term.absfree/absdummy; eliminated obsolete Term.list_abs_free;
2010-12-08 haftmann 2010-12-08 primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
2010-11-15 bulwahn 2010-11-15 ignoring the constant STR in the predicate compiler
2010-10-21 bulwahn 2010-10-21 adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
2010-09-23 bulwahn 2010-09-23 handling equivalences smarter in the predicate compiler
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-06-28 haftmann 2010-06-28 merged constants "split" and "prod_case"
2010-04-21 bulwahn 2010-04-21 added further inlining of boolean constants to the predicate compiler
2010-04-21 bulwahn 2010-04-21 added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
2010-03-31 bulwahn 2010-03-31 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
2010-03-24 bulwahn 2010-03-24 moved further predicate compile files to HOL-Library