| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 14:46:13 +0100 |
wenzelm |
refute_params are given in *this* theory;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 22:08:53 +0100 |
wenzelm |
declare command keywords via theory header, including strict checking outside Pure;
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 12:17:19 +0200 |
blanchet |
reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 13:34:57 +0200 |
haftmann |
moved sledgehammer to Plain; tuned dependencies
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 22:45:09 +0200 |
blanchet |
move Metis into Plain
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 17:12:16 +0200 |
wenzelm |
just one refute.ML;
|
file |
diff |
annotate
|
| Mon, 14 Dec 2009 12:14:12 +0100 |
blanchet |
added "no_assms" option to Refute, and include structured proof assumptions by default;
|
file |
diff |
annotate
|
| Mon, 07 Dec 2009 11:46:13 +0100 |
blanchet |
avoid using "prop_logic.ML" and "sat_solver.ML" twice (the other occurrence being in "FunDef.thy");
|
file |
diff |
annotate
|
| Tue, 10 Nov 2009 16:11:37 +0100 |
haftmann |
tuned imports
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Fri, 06 Feb 2009 13:43:19 +0100 |
blanchet |
Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML +
|
file |
diff |
annotate
|
| Wed, 02 Apr 2008 15:58:57 +0200 |
haftmann |
tuned imports
|
file |
diff |
annotate
|
| Thu, 11 Jan 2007 01:34:23 +0100 |
webertj |
updated to mention the automatic unfolding of constants
|
file |
diff |
annotate
|
| Mon, 13 Nov 2006 15:43:09 +0100 |
haftmann |
moved upwars in HOL theory graph
|
file |
diff |
annotate
|