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;
2011-03-18 blanchet 2011-03-18 always destroy constructor patterns, since this seems to be always useful
2011-03-09 blanchet 2011-03-09 improved formula for specialization, to prevent needless specializations -- and removed dead code
2011-03-03 blanchet 2011-03-03 simplify "need" option's syntax
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-28 blanchet 2011-02-28 improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
2011-02-28 blanchet 2011-02-28 made "fixed_is_special_eligible_arg" smarter w.r.t. pairs, and fixed previous unintended behavior because "andalso" ties more tightly than "orelse"
2011-02-21 blanchet 2011-02-21 more work on "fix_datatype_vals" optimization (renamed "preconstruct")
2011-02-21 blanchet 2011-02-21 improve optimization
2011-02-21 blanchet 2011-02-21 tweaked Nitpick based on C++ memory model example
2011-02-21 blanchet 2011-02-21 renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
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-07 blanchet 2010-12-07 removed needless optimization for image -- there might be cases that benefit from it but there are others where it is clearly evil
2010-12-07 blanchet 2010-12-07 simplified special handling of set products
2010-12-07 blanchet 2010-12-07 fix special handling of set products
2010-12-07 blanchet 2010-12-07 use heuristic to determine whether to keep or drop an existing "let" -- and drop all higher-order lets
2010-10-25 wenzelm 2010-10-25 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
2010-09-24 wenzelm 2010-09-24 modernized structure Ord_List;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;