src/HOL/Tools/Nitpick/nitpick_util.ML
2017-06-06 wenzelm 2017-06-06 discontinued obsolete print mode;
2016-03-05 wenzelm 2016-03-05 tuned signature -- clarified modules;
2015-12-20 wenzelm 2015-12-20 renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
2015-12-01 blanchet 2015-12-01 removed needless ML function
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-01-24 wenzelm 2015-01-24 tuned signature;
2015-01-24 wenzelm 2015-01-24 tuned;
2014-11-07 wenzelm 2014-11-07 tuned;
2014-11-07 wenzelm 2014-11-07 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; plain value Outer_Syntax within theory: parsing requires current theory context; clarified name of Keyword.is_literal according to its semantics; eliminated pointless type Keyword.T; simplified @{command_spec}; clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
2014-10-08 wenzelm 2014-10-08 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
2014-05-22 blanchet 2014-05-22 reverted '|' features in MaSh -- these sounded like a good idea but never really worked
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 code
2014-01-20 blanchet 2014-01-20 have Nitpick lookup codatatypes
2013-12-19 blanchet 2013-12-19 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
2013-12-09 blanchet 2013-12-09 compile
2013-12-09 blanchet 2013-12-09 generate problems with type classes
2013-11-21 blanchet 2013-11-21 eliminated Sledgehammer's dependency on old-style datatypes
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-09-23 blanchet 2013-09-23 added "spy" option to Nitpick
2013-09-10 blanchet 2013-09-10 sorted out dependencies
2013-09-10 blanchet 2013-09-10 moved ML function closer to its remaining use
2013-08-13 wenzelm 2013-08-13 discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end; document antiquotations: renamed term style "isub" to "sub";
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-05-27 blanchet 2013-05-27 get rid of "show_all_types" in Nitpick
2013-05-16 blanchet 2013-05-16 tuning -- renamed '_from_' to '_of_' in Sledgehammer
2012-12-15 blanchet 2012-12-15 thread no timeout properly
2012-10-31 blanchet 2012-10-31 moved Refute to "HOL/Library" to speed up building "Main" even more
2012-09-08 blanchet 2012-09-08 TODOs
2012-07-27 blanchet 2012-07-27 nicer Nitpick subscript output in jEdit
2012-07-18 blanchet 2012-07-18 optimized MaSh output by chunking it
2012-04-22 blanchet 2012-04-22 handle exception (needed to solve TPTP problem SEU880^5)
2012-02-27 wenzelm 2012-02-27 more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
2011-12-16 wenzelm 2011-12-16 tuned signature;
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-27 blanchet 2011-05-27 use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
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-01 blanchet 2011-05-01 shorten readable names -- they can get really long with monomorphization, which actually slows down the ATPs
2010-11-26 wenzelm 2010-11-26 make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
2010-11-20 wenzelm 2010-11-20 renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-11-03 blanchet 2010-11-03 standardize on seconds for Nitpick and Sledgehammer timeouts
2010-09-05 wenzelm 2010-09-05 turned show_sorts/show_types into proper configuration options;
2010-09-03 wenzelm 2010-09-03 turned show_all_types into proper configuration option;
2010-08-23 blanchet 2010-08-23 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later; it's a mistake to transform the elim rules too early because then we lose some info, e.g. "no_atp" attributes
2010-08-06 blanchet 2010-08-06 local versions of Nitpick.register_xxx functions
2010-08-05 blanchet 2010-08-05 fiddle with specialization etc.
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-03 blanchet 2010-08-03 better "Pretty" handling
2010-07-27 blanchet 2010-07-27 remove unused fun
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-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-27 blanchet 2010-04-27 remove Nitpick functions that are now implemented in Sledgehammer
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-03-23 blanchet 2010-03-23 leverage code now in Sledgehammer
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