src/HOL/Tools/Predicate_Compile/core_data.ML
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-07-27 wenzelm 2013-07-27 standardized aliases;
2013-05-30 wenzelm 2013-05-30 standardized aliases;
2012-11-12 haftmann 2012-11-12 dropped dead code
2012-01-14 wenzelm 2012-01-14 discontinued old-style Term.list_abs in favour of plain Term.abs;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-03-13 wenzelm 2011-03-13 tuned headers;
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-12-17 wenzelm 2010-12-17 refer to regular structure Simplifier;
2010-10-25 bulwahn 2010-10-25 using mode_eq instead of op = for lookup in the predicate compiler
2010-10-22 bulwahn 2010-10-22 moving general functions from core_data to predicate_compile_aux
2010-10-21 bulwahn 2010-10-21 using a signature in core_data and moving some more functions to core_data
2010-10-21 bulwahn 2010-10-21 splitting large core file into core_data, mode_inference and predicate_compile_proof