src/HOL/Tools/refute.ML
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;
Tue, 23 Jun 2009 16:27:12 +0200 haftmann tuned interfaces of datatype module
Sun, 21 Jun 2009 08:38:58 +0200 haftmann simplified names of common datatype types
Fri, 19 Jun 2009 17:23:21 +0200 haftmann discontinued ancient tradition to suffix certain ML module names with "_package"
Wed, 11 Mar 2009 15:56:51 +0100 haftmann HOLogic.mk_set, HOLogic.dest_set
Sat, 07 Mar 2009 16:47:36 +0100 blanchet Added a second timeout mechanism to Refute.
Sat, 07 Mar 2009 12:26:56 +0100 blanchet Refute: Distinguish between "genuine" and "potential" in the newly added "expect" option.
Fri, 06 Mar 2009 19:37:31 +0100 blanchet Added "expect" option to Refute, like in Nitpick, that allows to write regression tests.
Fri, 06 Mar 2009 17:21:17 +0100 blanchet Fix remaining occurrences of "'a set" in Refute, by using "'a => bool" instead.
Fri, 06 Mar 2009 11:10:57 +0100 haftmann merged
Thu, 05 Mar 2009 08:24:28 +0100 haftmann merged
Thu, 05 Mar 2009 08:23:11 +0100 haftmann set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
Thu, 05 Mar 2009 10:19:51 +0100 blanchet Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:43:39 +0100 blanchet Made Refute.norm_rhs public, so I can use it in Nitpick.
Sun, 01 Mar 2009 23:36:12 +0100 wenzelm use long names for old-style fold combinators;
Tue, 17 Feb 2009 14:01:54 +0100 blanchet Reintroduce set_interpreter for Collect and op :.
Fri, 06 Feb 2009 13:43:19 +0100 blanchet Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML +
Wed, 04 Feb 2009 18:10:07 +0100 blanchet Make some Refute functions public so I can use them in Nitpick,
Thu, 01 Jan 2009 14:23:39 +0100 wenzelm avoid polymorphic equality;
Wed, 31 Dec 2008 18:53:17 +0100 wenzelm use regular Term.add_XXX etc.;
Wed, 31 Dec 2008 00:08:13 +0100 wenzelm moved old add_term_vars, add_term_frees etc. to structure OldTerm;
less more (0) -100 -60 tip