src/HOL/Tools/Nitpick/nitpick_preproc.ML
2014-03-03 blanchet 2014-03-03 removed nonstandard models from Nitpick
2013-04-15 blanchet 2013-04-15 not all Nitpick 'constructors' are injective -- careful
2013-04-10 wenzelm 2013-04-10 more standard module name Axclass (according to file name);
2012-05-11 blanchet 2012-05-11 fixed "real" after they were redefined as a 'quotient_type'
2012-04-25 blanchet 2012-04-25 remove too aggressive skolemization optimization (prevented discovery of a model in SYN994^1)
2012-04-22 blanchet 2012-04-22 fix bug where "==" was used instead of "HOL.eq"
2012-01-04 blanchet 2012-01-04 improved "set" support by code inspection
2012-01-03 blanchet 2012-01-03 more robust destruction of "set Collect" idiom
2011-08-17 wenzelm 2011-08-17 modernized signature of Term.absfree/absdummy; eliminated obsolete Term.list_abs_free;
2011-04-19 blanchet 2011-04-19 use "Spec_Rules" for finding axioms -- more reliable and cleaner
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-03-18 blanchet 2011-03-18 always destroy constructor patterns, since this seems to be always useful
2011-03-03 blanchet 2011-03-03 simplify "need" option's syntax
2011-03-03 blanchet 2011-03-03 renamed "preconstr" option "need"
2011-03-02 blanchet 2011-03-02 unfold definitions in "preconstrs" option
2011-02-28 blanchet 2011-02-28 improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
2011-02-21 blanchet 2011-02-21 more work on "fix_datatype_vals" optimization (renamed "preconstruct")
2011-02-21 blanchet 2011-02-21 tweaked Nitpick based on C++ memory model example
2011-02-21 blanchet 2011-02-21 always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp"
2010-12-07 blanchet 2010-12-07 remove the "fin_fun" optimization in Nitpick -- it was always a hack and didn't help much
2010-12-06 blanchet 2010-12-06 removed old baggage from monotonicity calculus -- the "calculus" option didn't really work anyway because of on-the-fly simplifications
2010-12-06 blanchet 2010-12-06 support 3 monotonicity calculi in one and fix soundness bug
2010-11-26 wenzelm 2010-11-26 make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
2010-09-24 wenzelm 2010-09-24 modernized structure Ord_List;
2010-09-14 blanchet 2010-09-14 eliminate more clutter related to "fast_descrs" optimization
2010-09-14 blanchet 2010-09-14 remove "fast_descs" option from Nitpick; the option has been unsound for over a year and is too imprecise to be of any use when made sound
2010-09-13 blanchet 2010-09-13 remove unreferenced identifiers
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-26 haftmann 2010-08-26 formerly unnamed infix impliciation now named HOL.implies
2010-08-06 blanchet 2010-08-06 local versions of Nitpick.register_xxx functions
2010-08-06 blanchet 2010-08-06 quotient types registered as codatatypes are no longer quotient types
2010-08-05 blanchet 2010-08-05 added support for "Abs_" and "Rep_" functions on quotient types
2010-08-05 blanchet 2010-08-05 fiddle with specialization etc.
2010-08-05 blanchet 2010-08-05 handle inductive predicates correctly after change in "def" semantics
2010-08-05 blanchet 2010-08-05 don't specialize built-ins or constructors
2010-08-05 blanchet 2010-08-05 prevent the expansion of too large definitions -- use equations for these instead
2010-08-04 blanchet 2010-08-04 get rid of all "optimizations" regarding "unit" and other cardinality-1 types
2010-08-03 blanchet 2010-08-03 handle free variables even more gracefully; 1. show those that only occur in assumptions as part of the constants; 2. make sure locally defined Frees are given an Opt rep, just like constants generally owuld
2010-08-03 blanchet 2010-08-03 optimize local "def"s by treating them as definitions
2010-08-02 blanchet 2010-08-02 fix Skolemizer -- last week's optimizations resulted in UnequalLengths errors
2010-08-02 blanchet 2010-08-02 prevent generation of needless specialized constants etc.
2010-07-21 blanchet 2010-07-21 do a better job at Skolemizing in Nitpick, for TPTP FOF
2010-07-03 blanchet 2010-07-03 adapt Nitpick to "prod_case" and "*" -> "sum" renaming; the code in "Nitpick_Preproc", which sorted the types using "typ_ord", was wrong and evil; it seems to have worked only because "*" was called "*"
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-06-21 blanchet 2010-06-21 optimized code generated for datatype cases + more; more = lazy creation of debugging messages in mono code + use of "let" when performing some beta-applications (to avoid exponential blowup) + removal of some set constructs, to simplify the code and increase precision in some cases (and decrease it in others, but this can be regained)
2010-06-01 blanchet 2010-06-01 fix Nitpick soundness bug regarding The and Eps
2010-06-01 blanchet 2010-06-01 added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
2010-06-01 blanchet 2010-06-01 thread along context instead of theory for typedef lookup
2010-05-31 blanchet 2010-05-31 don't include any axioms for "TYPE" in Nitpick
2010-04-29 blanchet 2010-04-29 expand combinators in Isar proofs constructed by Sledgehammer; this requires shuffling around a couple of functions previously defined in Refute
2010-04-25 blanchet 2010-04-25 remove "skolemize" option from Nitpick, since Skolemization is always useful
2010-04-24 blanchet 2010-04-24 removed Nitpick's "uncurry" option
2010-04-24 blanchet 2010-04-24 remove type annotations as comments; Nitpick is now 1136 lines shorter
2010-04-24 blanchet 2010-04-24 cosmetics
2010-03-19 blanchet 2010-03-19 move the Sledgehammer Isar commands together into one file; this will make easier to add options and reorganize them later
2010-03-17 blanchet 2010-03-17 added support for "specification" and "ax_specification" constructs to Nitpick
2010-03-11 blanchet 2010-03-11 moved some Nitpick code around
2010-03-09 blanchet 2010-03-09 more work on Nitpick's finite sets
2010-03-09 blanchet 2010-03-09 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"