src/HOL/Tools/Nitpick/nitpick_hol.ML
Sat, 24 Dec 2011 16:14:58 +0100 haftmann adjusted to set/pred distinction by means of type constructor `set`
Fri, 09 Dec 2011 14:14:37 +0100 kuncar make ctxt the first parameter
Thu, 27 Oct 2011 21:02:10 +0200 wenzelm localized quotient data;
Thu, 27 Oct 2011 20:26:38 +0200 wenzelm simplified/standardized signatures;
Thu, 27 Oct 2011 13:50:54 +0200 bulwahn respecting isabelle's programming style in the quotient package by simplifying quotdata_lookup function for data access
Wed, 17 Aug 2011 18:05:31 +0200 wenzelm modernized signature of Term.absfree/absdummy;
Tue, 02 Aug 2011 13:07:00 +0200 krauss updated unchecked forward reference
Tue, 02 Aug 2011 12:27:24 +0200 krauss replaced Nitpick's hardwired basic_ersatz_table by context data
Tue, 02 Aug 2011 10:36:50 +0200 krauss moved recdef package to HOL/Library/Old_Recdef.thy
Tue, 02 Aug 2011 10:03:14 +0200 krauss added dynamic ersatz_table to Nitpick's data slot
Thu, 14 Jul 2011 16:50:05 +0200 blanchet added option to control which lambda translation to use (for experiments)
Tue, 31 May 2011 16:38:36 +0200 blanchet first step in sharing more code between ATP and Metis translation
Tue, 24 May 2011 00:01:33 +0200 blanchet fixed de Bruijn index bug
Fri, 13 May 2011 22:55:00 +0200 wenzelm proper Proof.context for classical tactics;
Thu, 05 May 2011 12:40:48 +0200 blanchet query typedefs as well for monotonicity
Wed, 04 May 2011 19:35:48 +0200 blanchet exploit inferred monotonicity
Wed, 04 May 2011 18:48:25 +0200 blanchet [mq]: nitpick_tuning
Wed, 04 May 2011 18:43:42 +0200 blanchet fixed cardinality computation for function types such as "'a -> unit"
Wed, 20 Apr 2011 13:54:07 +0200 wenzelm added Theory.nodes_of convenience;
Tue, 19 Apr 2011 14:38:38 +0200 blanchet 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
Tue, 19 Apr 2011 14:04:58 +0200 blanchet use "Spec_Rules" for finding axioms -- more reliable and cleaner
Tue, 19 Apr 2011 12:22:59 +0200 blanchet optimize trivial equalities early in Nitpick -- it shouldn't be the job of the peephole optimizer
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Fri, 18 Mar 2011 10:17:37 +0100 blanchet always destroy constructor patterns, since this seems to be always useful
Wed, 09 Mar 2011 10:28:01 +0100 blanchet improved formula for specialization, to prevent needless specializations -- and removed dead code
Thu, 03 Mar 2011 11:20:48 +0100 blanchet simplify "need" option's syntax
Thu, 03 Mar 2011 11:20:48 +0100 blanchet renamed "preconstr" option "need"
Wed, 02 Mar 2011 14:50:16 +0100 blanchet lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
Mon, 28 Feb 2011 17:53:10 +0100 blanchet improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
Mon, 28 Feb 2011 17:53:10 +0100 blanchet made "fixed_is_special_eligible_arg" smarter w.r.t. pairs, and fixed previous unintended behavior because "andalso" ties more tightly than "orelse"
Mon, 21 Feb 2011 17:36:32 +0100 blanchet more work on "fix_datatype_vals" optimization (renamed "preconstruct")
Mon, 21 Feb 2011 11:50:38 +0100 blanchet improve optimization
Mon, 21 Feb 2011 11:50:31 +0100 blanchet tweaked Nitpick based on C++ memory model example
Mon, 21 Feb 2011 10:44:19 +0100 blanchet renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
Mon, 21 Feb 2011 10:42:29 +0100 blanchet always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp"
Sat, 08 Jan 2011 17:14:48 +0100 wenzelm misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
Tue, 07 Dec 2010 11:56:53 +0100 blanchet remove the "fin_fun" optimization in Nitpick -- it was always a hack and didn't help much
Tue, 07 Dec 2010 11:56:01 +0100 blanchet removed needless optimization for image -- there might be cases that benefit from it but there are others where it is clearly evil
Tue, 07 Dec 2010 11:56:01 +0100 blanchet simplified special handling of set products
Tue, 07 Dec 2010 11:56:01 +0100 blanchet fix special handling of set products
Tue, 07 Dec 2010 11:56:01 +0100 blanchet use heuristic to determine whether to keep or drop an existing "let" -- and drop all higher-order lets
Mon, 25 Oct 2010 21:06:56 +0200 wenzelm renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
Fri, 24 Sep 2010 15:53:13 +0200 wenzelm modernized structure Ord_List;
Mon, 20 Sep 2010 16:05:25 +0200 wenzelm renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
Tue, 14 Sep 2010 13:44:43 +0200 blanchet eliminate more clutter related to "fast_descrs" optimization
Tue, 14 Sep 2010 13:24:18 +0200 blanchet remove "fast_descs" option from Nitpick;
Mon, 13 Sep 2010 20:21:40 +0200 blanchet remove unreferenced identifiers
Sat, 11 Sep 2010 10:13:51 +0200 blanchet always handle type variables in typedefs as global
Sat, 28 Aug 2010 16:14:32 +0200 haftmann formerly unnamed infix equality now named HOL.eq
Fri, 27 Aug 2010 10:56:46 +0200 haftmann formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
Thu, 26 Aug 2010 20:51:17 +0200 haftmann formerly unnamed infix impliciation now named HOL.implies
Mon, 23 Aug 2010 14:54:17 +0200 blanchet perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
Mon, 09 Aug 2010 12:40:15 +0200 blanchet use "declaration" instead of "setup" to register Nitpick extensions
Mon, 09 Aug 2010 12:05:48 +0200 blanchet move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
Fri, 06 Aug 2010 18:11:30 +0200 blanchet added support for partial quotient types;
Fri, 06 Aug 2010 17:23:11 +0200 blanchet adapt occurrences of renamed Nitpick functions
Fri, 06 Aug 2010 17:05:29 +0200 blanchet local versions of Nitpick.register_xxx functions
Fri, 06 Aug 2010 11:35:10 +0200 blanchet quotient types registered as codatatypes are no longer quotient types
Fri, 06 Aug 2010 10:50:52 +0200 blanchet improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type"
Thu, 05 Aug 2010 20:17:50 +0200 blanchet added "whack"
less more (0) -100 -60 tip