src/HOL/Tools/Nitpick/nitpick_hol.ML
2013-11-10 haftmann 2013-11-10 dropped obsolete check: dest_num always yields positive number
2013-09-24 blanchet 2013-09-24 encode goal digest in spying log (to detect duplicates)
2013-09-23 blanchet 2013-09-23 don't generalize w.r.t. wrong context -- better overgeneralize (since the instantiation phase will compensate for it)
2013-05-28 blanchet 2013-05-28 don't create needless constant
2013-04-15 blanchet 2013-04-15 not all Nitpick 'constructors' are injective -- careful
2013-02-15 haftmann 2013-02-15 two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one
2012-10-31 blanchet 2012-10-31 moved Refute to "HOL/Library" to speed up building "Main" even more
2012-10-12 wenzelm 2012-10-12 discontinued typedef with implicit set_def;
2012-08-15 blanchet 2012-08-15 fixed handling of "int" in the wake of its port to the quotient package
2012-08-15 blanchet 2012-08-15 removed dead code
2012-05-24 blanchet 2012-05-24 fixed soundness bug in Nitpick related to unfolding -- the unfolding criterion must at least as strict when looking at a definitional axiom as elsewhere, otherwise we end up unfolding a constant's definition in its own definition, yielding a trivial equality
2012-05-11 blanchet 2012-05-11 fixed "real" after they were redefined as a 'quotient_type'
2012-04-26 blanchet 2012-04-26 fixed bug in handling of new numerals -- the left-hand side of "Numeral1 = 1" should be left alone and not translated to a built-in Kodkod numeral in the specification of the "numeral" function
2012-04-22 blanchet 2012-04-22 more meaningful default value
2012-04-22 blanchet 2012-04-22 handle exception (needed to solve TPTP problem SEU880^5)
2012-04-03 griff 2012-04-03 renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
2012-03-26 blanchet 2012-03-26 fixed Nitpick after numeral representation change (2a1953f0d20d)
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-03-04 blanchet 2012-03-04 addressed a quotient-type-related issue that arose with the port to "set"
2012-03-01 blanchet 2012-03-01 improved handling of polymorphic quotient types, by avoiding comparing types that will generally differ in the polymorphic case
2012-03-01 blanchet 2012-03-01 fixed handling of "Rep_" function of quotient types -- side-effect of "set" constructor reintroduction
2012-01-23 blanchet 2012-01-23 renamed two files to make room for a new file
2012-01-17 blanchet 2012-01-17 fixed a bug introduced when porting functions to set -- extensionality on sets break the form of equations expected elsewhere by Nitpick
2012-01-14 wenzelm 2012-01-14 discontinued old-style Term.list_abs in favour of plain Term.abs;
2012-01-14 wenzelm 2012-01-14 renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
2012-01-04 blanchet 2012-01-04 improved "set" support by code inspection
2012-01-04 blanchet 2012-01-04 tuning
2012-01-03 blanchet 2012-01-03 fixed bisimilarity axiom -- avoid "insert" with wrong type
2012-01-03 blanchet 2012-01-03 more robust destruction of "set Collect" idiom
2012-01-03 blanchet 2012-01-03 handle starred predicates correctly w.r.t. "set"
2012-01-03 blanchet 2012-01-03 simplify mem Collect
2012-01-03 blanchet 2012-01-03 fixed set extensionality code
2012-01-03 blanchet 2012-01-03 construct correct "set" type for wf goal
2012-01-03 blanchet 2012-01-03 fixed Nitpick's typedef handling w.r.t. "set"
2012-01-03 blanchet 2012-01-03 rationalized output (a bit)
2012-01-03 blanchet 2012-01-03 port part of Nitpick to "set" type constructor
2012-01-03 blanchet 2012-01-03 ported mono calculus to handle "set" type constructors
2011-12-24 haftmann 2011-12-24 adjusted to set/pred distinction by means of type constructor `set`
2011-12-09 kuncar 2011-12-09 make ctxt the first parameter
2011-10-27 wenzelm 2011-10-27 localized quotient data;
2011-10-27 wenzelm 2011-10-27 simplified/standardized signatures;
2011-10-27 bulwahn 2011-10-27 respecting isabelle's programming style in the quotient package by simplifying quotdata_lookup function for data access
2011-08-17 wenzelm 2011-08-17 modernized signature of Term.absfree/absdummy; eliminated obsolete Term.list_abs_free;
2011-08-02 krauss 2011-08-02 updated unchecked forward reference
2011-08-02 krauss 2011-08-02 replaced Nitpick's hardwired basic_ersatz_table by context data
2011-08-02 krauss 2011-08-02 moved recdef package to HOL/Library/Old_Recdef.thy
2011-08-02 krauss 2011-08-02 added dynamic ersatz_table to Nitpick's data slot
2011-07-14 blanchet 2011-07-14 added option to control which lambda translation to use (for experiments)
2011-05-31 blanchet 2011-05-31 first step in sharing more code between ATP and Metis translation
2011-05-24 blanchet 2011-05-24 fixed de Bruijn index bug
2011-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
2011-05-05 blanchet 2011-05-05 query typedefs as well for monotonicity
2011-05-04 blanchet 2011-05-04 exploit inferred monotonicity
2011-05-04 blanchet 2011-05-04 [mq]: nitpick_tuning
2011-05-04 blanchet 2011-05-04 fixed cardinality computation for function types such as "'a -> unit"
2011-04-20 wenzelm 2011-04-20 added Theory.nodes_of convenience;
2011-04-19 blanchet 2011-04-19 avoid relying on "Thm.definitionK" to pick up definitions -- this was an old hack related to locales (to avoid expanding locale constants to their low-level definition) that is no longer necessary
2011-04-19 blanchet 2011-04-19 use "Spec_Rules" for finding axioms -- more reliable and cleaner
2011-04-19 blanchet 2011-04-19 optimize trivial equalities early in Nitpick -- it shouldn't be the job of the peephole optimizer
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;