src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
2015-07-08 wenzelm 2015-07-08 clarified context;
2015-06-03 wenzelm 2015-06-03 clarified context;
2015-03-06 wenzelm 2015-03-06 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local 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;
2015-02-05 haftmann 2015-02-05 slightly more standard code setup for String.literal, with explicit special case in predicate compiler
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-26 wenzelm 2014-11-26 added ML antiquotation @{apply n} or @{apply n(k)};
2014-08-16 wenzelm 2014-08-16 updated to named_theorems;
2014-03-23 wenzelm 2014-03-23 more sensible treatment of quasi-local variables (NB: Variable.add_fixes is only for term variables, while Variable.declare takes care of types within given terms);
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-21 wenzelm 2014-03-21 tuned signature;
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 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-09-25 blanchet 2013-09-25 filled in gap in library offering
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;
2013-02-28 wenzelm 2013-02-28 just one HOLogic.Trueprop_conv, with regular exception CTERM; tuned;
2012-11-12 haftmann 2012-11-12 dropped dead code
2012-07-09 bulwahn 2012-07-09 adding a missing entry to predicate compiler's setup
2012-02-24 haftmann 2012-02-24 dropped dead code
2012-02-24 haftmann 2012-02-24 given up disfruitful branch
2012-02-23 haftmann 2012-02-23 dropped dead code
2011-12-17 wenzelm 2011-12-17 tuned signature;
2011-12-14 wenzelm 2011-12-14 avoid fragile Sign.intern_const -- pass internal names directly; tuned;
2011-12-12 wenzelm 2011-12-12 datatype dtyp with explicit sort information; tuned messages;
2011-11-30 wenzelm 2011-11-30 discontinued obsolete datatype "alt_names";
2011-11-11 bulwahn 2011-11-11 using more conventional names for monad plus operations
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-08-17 wenzelm 2011-08-17 modernized signature of Term.absfree/absdummy; eliminated obsolete Term.list_abs_free;
2011-06-09 wenzelm 2011-06-09 simplified Name.variant -- discontinued builtin fold_map;
2011-06-09 wenzelm 2011-06-09 discontinued Name.variant to emphasize that this is old-style / indirect;
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;
2011-03-24 bulwahn 2011-03-24 allowing special set comprehensions in values command; adding an example for special set comprehension in values
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-12-01 wenzelm 2010-12-01 more direct use of binder_types/body_type;
2010-10-25 bulwahn 2010-10-25 renaming split_modeT' to split_modeT
2010-10-22 bulwahn 2010-10-22 moving general functions from core_data to predicate_compile_aux
2010-10-21 bulwahn 2010-10-21 adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
2010-10-21 bulwahn 2010-10-21 splitting large core file into core_data, mode_inference and predicate_compile_proof
2010-10-21 bulwahn 2010-10-21 added generator_dseq compilation for a sound depth-limited compilation with small value generators
2010-10-21 bulwahn 2010-10-21 adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
2010-10-21 bulwahn 2010-10-21 adding option smart_depth_limiting to predicate compiler
2010-09-30 bulwahn 2010-09-30 applying case beta reduction to case term before matching in predicate compile function flattening; moving case beta reduction function to Predicate_Compile_Aux
2010-09-29 bulwahn 2010-09-29 adding splitting of conjuncts in assumptions as forward rule on theorems; replacing term transformation for splitting conjuncts by theorem transformation; removing obsolete functions; tuned
2010-09-23 bulwahn 2010-09-23 removing unneccessary expansion procedure for elimination rules; removing obsolete elim preprocessing; tuned
2010-09-23 bulwahn 2010-09-23 moving the preprocessing of introduction rules after the code_pred command; added tuple expansion preprocessing of elimination rule
2010-09-20 bulwahn 2010-09-20 removing clone in code_prolog and predicate_compile_quickcheck
2010-09-15 bulwahn 2010-09-15 adding option show_invalid_clauses for a more detailed message when modes are not inferred
2010-09-15 bulwahn 2010-09-15 proposed modes for code_pred now supports modes for mutual predicates
2010-09-13 bulwahn 2010-09-13 handling function types more carefully than in e98a06145530
2010-09-13 bulwahn 2010-09-13 adding order on modes
2010-09-10 bulwahn 2010-09-10 directly computing the values of interest instead of composing functions in an unintelligent way that causes exponential much garbage; using the latest theory
2010-09-07 bulwahn 2010-09-07 raising an exception instead of guessing some reasonable behaviour for this function