src/HOL/ex/predicate_compile.ML
2009-05-16 bulwahn 2009-05-16 added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
2009-05-15 bulwahn 2009-05-15 added predicate transformation function for code generation
2009-05-15 bulwahn 2009-05-15 added predicate transformation function for code generation
2009-05-14 haftmann 2009-05-14 merged module code_unit.ML into code.ML
2009-05-12 haftmann 2009-05-12 marginally tuned
2009-05-11 haftmann 2009-05-11 fixed merge accident
2009-05-11 haftmann 2009-05-11 merged
2009-05-11 bulwahn 2009-05-11 fixed code_pred command
2009-05-11 bulwahn 2009-05-11 Added pred_code command
2009-04-22 bulwahn 2009-04-22 added general preprocessing of equality in predicates for code generation
2009-04-24 haftmann 2009-04-24 some experiements towards user interface for predicate compiler
2009-03-15 wenzelm 2009-03-15 simplified attribute setup;
2009-03-09 haftmann 2009-03-09 NameSpace.base_name ~> Long_Name.base_name
2009-03-09 haftmann 2009-03-09 binding replaces bstring
2009-03-08 haftmann 2009-03-08 added predicate compiler, as formally checked prototype, not as user package