src/HOL/Tools/Nitpick/nitpick_hol.ML
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-01-24 wenzelm 2015-01-24 tuned signature;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-24 blanchet 2014-11-24 no need for subset operation as a primitive in Nitpick, esp. that its implementation was unsound (cf. Rene Thiemann's 16 Oct 2014 email on isabelle mailing list)
2014-10-31 wenzelm 2014-10-31 discontinued obsolete Output.urgent_message;
2014-10-08 wenzelm 2014-10-08 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
2014-08-19 blanchet 2014-08-19 tuning
2014-08-16 wenzelm 2014-08-16 updated to named_theorems;
2014-06-12 blanchet 2014-06-12 removed subsumed record-related code, now that records are registered as 'ctr_sugar'
2014-06-12 blanchet 2014-06-12 made lookup more robust in the face of missing (dummy) case constant
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-19 wenzelm 2014-03-19 more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
2014-03-15 wenzelm 2014-03-15 tuned signature; eliminated clones;
2014-03-03 blanchet 2014-03-03 fixed handling of 'case_prod' and other 'case' functions for interpreted types
2014-03-03 blanchet 2014-03-03 support 'datatype_new'-defined datatypes in Nitpick + better support for 'codatatype's
2014-03-03 blanchet 2014-03-03 tuned ML names
2014-03-03 blanchet 2014-03-03 tuned code
2014-03-03 blanchet 2014-03-03 removed nonstandard models from Nitpick
2014-03-03 blanchet 2014-03-03 guard against unsound cases that arise when people peek into 'int' and similar types that are handled specially by Nitpick
2014-02-19 blanchet 2014-02-19 adapted Nitpick to 'primrec' refactoring
2014-02-17 blanchet 2014-02-17 simplified data structure by reducing the incidence of clumsy indices
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-01-20 blanchet 2014-01-20 have Nitpick lookup codatatypes
2014-01-16 blanchet 2014-01-16 adapted to move of Wfrec
2013-12-19 blanchet 2013-12-19 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
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