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
2010-03-22 bulwahn 2010-03-22 a new simpler random compilation for the predicate compiler
2010-03-22 bulwahn 2010-03-22 reviving the classical depth-limited computation in the predicate compiler
2010-03-22 bulwahn 2010-03-22 restructuring function flattening
2010-03-07 wenzelm 2010-03-07 modernized structure Local_Defs;
2010-02-27 wenzelm 2010-02-27 just one copy of structure Term_Graph (in Pure);
2010-02-25 bulwahn 2010-02-25 adding no_topmost_reordering as new option to the code_pred command
2010-02-23 bulwahn 2010-02-23 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
2010-02-19 haftmann 2010-02-19 simplified
2010-01-20 bulwahn 2010-01-20 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
2009-11-19 bulwahn 2009-11-19 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
2009-11-12 bulwahn 2009-11-12 new names for predicate functions in the predicate compiler * * * adopting examples of the predicate compiler
2009-11-12 bulwahn 2009-11-12 changed modes to expected_modes; added UNION to code_pred_inlining; fixed some examples; tuned
2009-11-12 bulwahn 2009-11-12 added interface of user proposals for names of generated constants
2009-11-12 bulwahn 2009-11-12 first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
2009-11-06 bulwahn 2009-11-06 adding tracing function for evaluated code; annotated compilation in the predicate compiler
2009-10-30 bulwahn 2009-10-30 renamed rpred to random
2009-10-28 bulwahn 2009-10-28 moved datatype mode and string functions to the auxillary structure
2009-10-28 bulwahn 2009-10-28 improving mode parsing in the predicate compiler
2009-10-28 wenzelm 2009-10-28 proper headers;
2009-10-27 bulwahn 2009-10-27 added option show_modes to predicate compiler
2009-10-27 bulwahn 2009-10-27 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck