src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
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