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-05-30 wenzelm 2013-05-30 standardized aliases;
2013-05-24 wenzelm 2013-05-24 tuned signature;
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-03-13 wenzelm 2012-03-13 more explicit indication of def names;
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;
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
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-27 bulwahn 2010-09-27 handling nested cases more elegant by requiring less new constants
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-16 bulwahn 2010-09-16 improving replacing higher order arguments to work with tuples
2010-08-31 bulwahn 2010-08-31 avoiding warning for a duplicate rewrite rule in preprocessing of the predicate compiler
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 use antiquotations for remaining unqualified constants in HOL
2010-07-21 bulwahn 2010-07-21 putting proof in the right context; adding if rewriting; tuned
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-03-29 bulwahn 2010-03-29 removing fishing for split thm in the predicate compiler
2010-03-22 wenzelm 2010-03-22 eliminated old-style Drule.add_axiom in favour of Specification.axiom, with explicit Drule.export_without_context to imitate the old behaviour;
2010-03-22 bulwahn 2010-03-22 improving handling of case expressions in predicate rewriting
2010-03-22 wenzelm 2010-03-22 replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-01 bulwahn 2010-03-01 made smlnj happy
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-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-05 wenzelm 2009-11-05 eliminated funny record patterns and made SML/NJ happy;
2009-11-03 bulwahn 2009-11-03 recursively replacing abstractions by new definitions in the predicate compiler
2009-10-30 bulwahn 2009-10-30 renamed rpred to random
2009-10-28 wenzelm 2009-10-28 proper headers;
2009-10-27 bulwahn 2009-10-27 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck