src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.ML;
2015-09-04 wenzelm 2015-09-04 tuned -- do not open ML structures;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-07-08 wenzelm 2015-07-08 clarified context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2014-11-09 wenzelm 2014-11-09 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
2014-04-09 wenzelm 2014-04-09 proper context for print_tac;
2014-04-09 wenzelm 2014-04-09 more conventional tactic programming; tuned;
2014-02-21 blanchet 2014-02-21 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
2014-02-12 wenzelm 2014-02-12 merged, resolving some conflicts;
2014-02-12 wenzelm 2014-02-12 tuned whitespace;
2014-02-12 blanchet 2014-02-12 tuned message
2014-02-12 blanchet 2014-02-12 ported predicate compiler to 'ctr_sugar' * * * ported predicate compiler to 'ctr_sugar', part 2
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;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-03-27 wenzelm 2013-03-27 clarified Skip_Proof.cheat_tac: more standard tactic; clarified Method.cheating: check quick_and_dirty when it is actually applied;
2012-11-12 haftmann 2012-11-12 dropped dead code
2012-02-14 wenzelm 2012-02-14 eliminated obsolete aliases;
2011-11-30 wenzelm 2011-11-30 discontinued obsolete datatype "alt_names";
2011-11-27 wenzelm 2011-11-27 more antiquotations;
2011-11-11 bulwahn 2011-11-11 adding CPS compilation to predicate compiler; removing function_flattening reference; new testers smart_exhaustive and smart_slow_exhaustive; renaming PredicateCompFuns to Predicate_Comp_Funs;
2011-05-15 wenzelm 2011-05-15 eliminated obsolete "assert" function, including divergent (unused!?) clone in Predicate_Compile_Proof;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
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-21 bulwahn 2010-10-21 splitting large core file into core_data, mode_inference and predicate_compile_proof