src/HOL/Tools/Nitpick/nitpick_hol.ML
2010-08-06 blanchet 2010-08-06 improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type"
2010-08-05 blanchet 2010-08-05 added "whack"
2010-08-05 blanchet 2010-08-05 handle "Rep_unit" & Co. gracefully
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-05 blanchet 2010-08-05 make nitpick accept "==" for "nitpick_(p)simp"s
2010-08-05 blanchet 2010-08-05 fix bug in Nitpick's "equationalize" function (the prems were ignored) + make it do some basic extensionalization
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 better "Pretty" handling
2010-08-03 blanchet 2010-08-03 bump up the max cardinalities, to use up more of the time given to us by the user
2010-08-03 blanchet 2010-08-03 fix newly introduced bug w.r.t. conditional equations
2010-08-03 blanchet 2010-08-03 make Nitpick more flexible when parsing (p)simp rules
2010-08-03 blanchet 2010-08-03 optimize local "def"s by treating them as definitions
2010-08-02 blanchet 2010-08-02 careful about which linear inductive predicates should be starred
2010-08-02 blanchet 2010-08-02 prefer implication to equality, to be more SAT solver friendly
2010-08-02 blanchet 2010-08-02 fix bug with mutually recursive and nested codatatypes
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-06-28 haftmann 2010-06-28 merged constants "split" and "prod_case"
2010-06-21 blanchet 2010-06-21 sort cases on the proper key
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 cosmetics
2010-06-01 blanchet 2010-06-01 removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead
2010-06-01 blanchet 2010-06-01 honor xsymbols in Nitpick
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 make Nitpick handle multiple typedef entries for same typedef
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-05-31 blanchet 2010-05-31 fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
2010-04-30 blanchet 2010-04-30 catch the right exception
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 cosmetics
2010-04-25 blanchet 2010-04-25 remove "show_skolems" option and change style of record declarations
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-23 blanchet 2010-04-23 stop referring to Sledgehammer_Util stuff all over Nitpick code; instead, redeclare any needed function in Nitpick_Util as synonym for the Sledgehammer_Util function of the same name
2010-04-13 blanchet 2010-04-13 cosmetics
2010-03-29 blanchet 2010-03-29 get rid of Polyhash, since it's no longer used
2010-03-27 wenzelm 2010-03-27 Typedef.info: separate global and local part, only the latter is transformed by morphisms;
2010-03-22 blanchet 2010-03-22 detect OFCLASS() axioms in Nitpick; this is necessary now that "Thy.all_axioms_of" returns such axiom (starting with change 46cfc4b8112e)
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-17 blanchet 2010-03-17 added support for "specification" and "ax_specification" constructs to Nitpick
2010-03-13 wenzelm 2010-03-13 adapted to localized typedef: handle single global interpretation only;
2010-03-11 blanchet 2010-03-11 moved some Nitpick code around
2010-03-11 blanchet 2010-03-11 added term postprocessor to Nitpick, to provide custom syntax for typedefs
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"
2010-03-09 blanchet 2010-03-09 added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2010-02-26 blanchet 2010-02-26 use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
2010-02-26 blanchet 2010-02-26 more work on the new monotonicity stuff in Nitpick
2010-02-25 blanchet 2010-02-25 improved precision of infinite "shallow" datatypes in Nitpick; e.g. strings used for variable names, instead of an opaque type
2010-02-25 blanchet 2010-02-25 cosmetics
2010-02-23 blanchet 2010-02-23 support local definitions in Nitpick
2010-02-23 blanchet 2010-02-23 optimized multisets in Nitpick by fishing "finite"
2010-02-23 blanchet 2010-02-23 improved Nitpick's support for quotient types
2010-02-23 blanchet 2010-02-23 catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example