src/HOL/Tools/Nitpick/nitpick_model.ML
2017-06-06 wenzelm 2017-06-06 discontinued obsolete print mode;
2016-03-29 wenzelm 2016-03-29 more position information for type mixfix;
2015-10-07 blanchet 2015-10-07 avoid 'legacy binding' warning
2015-10-07 blanchet 2015-10-07 removed dead code
2015-10-06 blanchet 2015-10-06 compile
2015-10-06 blanchet 2015-10-06 avoid legacy syntax
2015-10-05 blanchet 2015-10-05 avoid unsound simplification of (C (s x)) when s is a selector but not C's
2015-08-13 wenzelm 2015-08-13 tuned signature, in accordance to sortBy in Scala;
2015-05-29 blanchet 2015-05-29 removed model checks from Nitpick
2015-04-22 blanchet 2015-04-22 avoid binding warning in Nitpick
2015-04-20 blanchet 2015-04-20 declare Nitpick atoms to avoid '??.' prefixes in output
2015-04-08 wenzelm 2015-04-08 proper context for Object_Logic operations;
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;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
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-03-22 wenzelm 2014-03-22 more antiquotations;
2014-03-19 wenzelm 2014-03-19 more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
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-02-24 wenzelm 2014-02-24 prefer standard Proof_Context.transfer, with theory stamp transfer (should now work thanks to purely functional theory, without Theory.copy etc.);
2013-12-19 blanchet 2013-12-19 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-07-18 wenzelm 2013-07-18 immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 -> 100000, JinjaThreads: 65000 -> 300000) -- minimal measurable impact on inference kernel performance;
2013-05-27 blanchet 2013-05-27 get rid of "show_all_types" in Nitpick
2012-07-18 blanchet 2012-07-18 optimized MaSh output by chunking it
2012-05-11 blanchet 2012-05-11 fixed "real" after they were redefined as a 'quotient_type'
2012-01-04 blanchet 2012-01-04 handle higher-order occurrences of sets gracefully in model display
2012-01-03 blanchet 2012-01-03 no abuse of notation
2012-01-03 blanchet 2012-01-03 create consts with proper "set" types
2012-01-03 blanchet 2012-01-03 port part of Nitpick to "set" type constructor
2011-11-13 blanchet 2011-11-13 avoid confusing selector output
2011-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
2011-04-19 blanchet 2011-04-19 use "Spec_Rules" for finding axioms -- more reliable and cleaner
2011-04-17 wenzelm 2011-04-17 report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-03-17 blanchet 2011-03-17 reintroduced "show_skolems" option -- useful when too many Skolems are displayed
2011-03-03 blanchet 2011-03-03 renamed "preconstr" option "need"
2011-03-02 blanchet 2011-03-02 lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
2011-02-21 blanchet 2011-02-21 more work on "fix_datatype_vals" optimization (renamed "preconstruct")
2011-02-21 blanchet 2011-02-21 always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp"
2011-01-08 wenzelm 2011-01-08 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
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 show strings as "s_1" etc. rather than "l_1" etc.
2010-11-20 wenzelm 2010-11-20 renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-10-25 wenzelm 2010-10-25 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
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-09-03 wenzelm 2010-09-03 turned show_all_types into proper configuration option;
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-09 blanchet 2010-08-09 use "declaration" instead of "setup" to register Nitpick extensions
2010-08-06 blanchet 2010-08-06 local versions of Nitpick.register_xxx functions
2010-08-05 blanchet 2010-08-05 added "whack"
2010-08-05 blanchet 2010-08-05 added support for "Abs_" and "Rep_" functions on quotient types
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 tuning
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