src/HOL/Tools/refute.ML
Sun, 17 Jul 2011 14:21:19 +0200 blanchet fixed lambda-liftg: must ensure the formulas are in close form
Tue, 31 May 2011 16:38:36 +0200 blanchet first step in sharing more code between ATP and Metis translation
Wed, 04 May 2011 19:35:48 +0200 blanchet exploit inferred monotonicity
Sat, 16 Apr 2011 18:11:20 +0200 wenzelm eliminated old List.nth;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Sun, 27 Mar 2011 16:56:16 +0200 krauss avoid *** in normal output, which usually marks errors in logs
Sat, 08 Jan 2011 17:14:48 +0100 wenzelm misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
Sat, 08 Jan 2011 16:01:51 +0100 wenzelm modernized structure Prop_Logic;
Fri, 26 Nov 2010 21:31:46 +0100 wenzelm explicit use of unprefix;
Sat, 20 Nov 2010 00:53:26 +0100 wenzelm renamed raw "explode" function to "raw_explode" to emphasize its meaning;
Mon, 25 Oct 2010 21:06:56 +0200 wenzelm renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
Fri, 01 Oct 2010 10:25:36 +0200 haftmann chop_while replace drop_while and take_while
Thu, 30 Sep 2010 18:37:29 +0200 haftmann take_while, drop_while
Fri, 03 Sep 2010 11:21:58 +0200 wenzelm turned show_consts into proper configuration option;
Fri, 03 Sep 2010 10:58:11 +0200 wenzelm prefer regular Proof.context over background theory;
Thu, 02 Sep 2010 17:12:16 +0200 wenzelm just one refute.ML;
Thu, 02 Sep 2010 16:45:21 +0200 wenzelm use existing Integer.pow, despite its slightly odd argument order;
Thu, 02 Sep 2010 16:31:50 +0200 wenzelm tuned whitespace and indentation, emphasizing the logical structure of this long text;
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
Thu, 19 Aug 2010 12:11:57 +0200 haftmann use HOLogic.boolT and @{typ bool} more pervasively
Thu, 01 Jul 2010 16:54:42 +0200 haftmann qualified constants Set.member and Set.Collect
Mon, 28 Jun 2010 15:32:25 +0200 haftmann avoid List.all
Fri, 11 Jun 2010 17:14:01 +0200 haftmann avoid references to old constdefs
Thu, 10 Jun 2010 12:24:03 +0200 haftmann tuned quotes, antiquotations and whitespace
Tue, 08 Jun 2010 16:37:22 +0200 haftmann tuned quotes, antiquotations and whitespace
Mon, 31 May 2010 18:49:32 +0200 blanchet move SAT solver warning from every invocation of SAT solver to the tool, Refute, that uses it;
Tue, 25 May 2010 20:28:16 +0200 wenzelm eliminated various catch-all exception patterns, guessing at the concrete exeptions that are intended here;
Wed, 05 May 2010 18:25:34 +0200 haftmann farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
Thu, 29 Apr 2010 01:17:14 +0200 blanchet expand combinators in Isar proofs constructed by Sledgehammer;
Fri, 23 Apr 2010 16:59:48 +0200 blanchet remove debugging code
Tue, 13 Apr 2010 15:16:54 +0200 blanchet commented out unsound "lfp"/"gfp" handling + fixed set output syntax;
Sat, 13 Mar 2010 15:12:56 +0100 wenzelm more antiquotations;
Fri, 19 Feb 2010 14:47:01 +0100 haftmann moved remaning class operations from Algebras.thy to Groups.thy
Wed, 10 Feb 2010 14:12:04 +0100 haftmann moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
Thu, 28 Jan 2010 11:48:49 +0100 haftmann new theory Algebras.thy for generic algebraic structures
Mon, 14 Dec 2009 12:14:12 +0100 blanchet added "no_assms" option to Refute, and include structured proof assumptions by default;
Mon, 07 Dec 2009 11:44:49 +0100 blanchet better error message in Refute when specifying a non-existing SAT solver
Mon, 30 Nov 2009 11:42:49 +0100 haftmann modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
Tue, 24 Nov 2009 17:28:25 +0100 haftmann curried take/drop
Sun, 08 Nov 2009 18:43:42 +0100 wenzelm adapted Theory_Data;
Thu, 29 Oct 2009 23:56:33 +0100 wenzelm eliminated some old folds;
Thu, 29 Oct 2009 17:58:26 +0100 wenzelm standardized filter/filter_out;
Tue, 27 Oct 2009 22:57:23 +0100 wenzelm eliminated some old folds;
Tue, 27 Oct 2009 17:34:00 +0100 wenzelm normalized basic type abbreviations;
Thu, 22 Oct 2009 13:48:06 +0200 haftmann map_range (and map_index) combinator
Wed, 21 Oct 2009 16:57:57 +0200 blanchet merged
Wed, 21 Oct 2009 16:54:04 +0200 blanchet fixed the "expect" mechanism of Refute in the face of timeouts
Wed, 21 Oct 2009 12:02:56 +0200 haftmann curried union as canonical list operation
Wed, 21 Oct 2009 08:16:25 +0200 haftmann merged
Wed, 21 Oct 2009 08:14:38 +0200 haftmann dropped redundant gen_ prefix
Tue, 20 Oct 2009 16:13:01 +0200 haftmann replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
Wed, 21 Oct 2009 00:36:12 +0200 wenzelm standardized basic operations on type option;
Mon, 19 Oct 2009 21:54:57 +0200 wenzelm uniform use of Integer.add/mult/sum/prod;
Thu, 15 Oct 2009 23:28:10 +0200 wenzelm replaced String.concat by implode;
Thu, 15 Oct 2009 21:28:39 +0200 wenzelm normalized aliases of Output operations;
Fri, 02 Oct 2009 21:41:57 +0200 wenzelm Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
Fri, 10 Jul 2009 07:59:27 +0200 haftmann dropped find_index_eq
Mon, 06 Jul 2009 19:58:52 +0200 wenzelm renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
less more (0) -100 -60 tip