src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
2012-03-25 ago merged fork with new numeral representation (see NEWS)
2012-03-13 ago prefer abs_def over def_raw;
2012-03-12 ago tuned proofs
2011-12-24 ago adjusted to set/pred distinction by means of type constructor `set`
2011-11-11 ago using more conventional names for monad plus operations
2011-10-21 ago replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
2011-09-14 ago renamed Complete_Lattices lemmas, removed legacy names
2011-09-12 ago new fastforce replacing fastsimp - less confusing name
2011-08-17 ago modernized signature of Term.absfree/absdummy;
2010-12-08 ago primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
2010-11-15 ago ignoring the constant STR in the predicate compiler
2010-10-21 ago adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
2010-09-23 ago handling equivalences smarter in the predicate compiler
2010-09-13 ago renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 ago expand_fun_eq -> ext_iff
2010-06-28 ago merged constants "split" and "prod_case"
2010-04-21 ago added further inlining of boolean constants to the predicate compiler
2010-04-21 ago added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
2010-03-31 ago 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 ago moved further predicate compile files to HOL-Library