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
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-19 haftmann 2010-08-19 tuned quotes
2010-08-19 haftmann 2010-08-19 tuned
2010-08-19 haftmann 2010-08-19 use antiquotations for remaining unqualified constants in HOL
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-06-10 haftmann 2010-06-10 tuned quotes, antiquotations and whitespace
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-21 bulwahn 2010-04-21 added switch detection to the predicate compiler
2010-04-21 bulwahn 2010-04-21 only add relevant predicates to the list of extra modes
2010-04-21 bulwahn 2010-04-21 added option for specialisation 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 iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
2010-03-31 bulwahn 2010-03-31 adding signature to Predicate_Compile_Aux; tuning Predicate_Compile_Aux structure
2010-03-31 bulwahn 2010-03-31 putting compilation setup of predicate compiler in a separate file
2010-03-29 bulwahn 2010-03-29 generalized alternative functions to alternative compilation to handle arithmetic functions better
2010-03-29 bulwahn 2010-03-29 adding registration of functions in the function flattening
2010-03-29 bulwahn 2010-03-29 adding specialisation of predicates to the predicate compiler
2010-03-29 bulwahn 2010-03-29 removing fishing for split thm in the predicate compiler
2010-03-29 bulwahn 2010-03-29 removing simple equalities in introduction rules in the predicate compiler
2010-03-29 bulwahn 2010-03-29 added new compilation to predicate_compiler
2010-03-22 bulwahn 2010-03-22 contextifying the compilation of the predicate compiler
2010-03-22 bulwahn 2010-03-22 some improvements thanks to Makarius source code review
2010-03-22 bulwahn 2010-03-22 adding depth_limited_random compilation to predicate compiler