| Thu, 14 Apr 2011 11:24:05 +0200 |
blanchet |
"unify_first_prem_with_concl" (cf. 9ceb585c097a) sometimes throws an exception, but it is very rarely needed -- catch the exception for now
|
file |
diff |
annotate
|
| Thu, 14 Apr 2011 11:24:05 +0200 |
blanchet |
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
|
file |
diff |
annotate
|
| Thu, 14 Apr 2011 11:24:04 +0200 |
blanchet |
removed obsolete Skolem counter in new Skolemizer
|
file |
diff |
annotate
|
| Thu, 14 Apr 2011 11:24:04 +0200 |
blanchet |
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
|
file |
diff |
annotate
|
| Thu, 14 Apr 2011 11:24:04 +0200 |
blanchet |
make new Skolemizer work also for "metisFT"
|
file |
diff |
annotate
|
| Thu, 14 Apr 2011 11:24:04 +0200 |
blanchet |
try to repair out-of-sync situations in Metis
|
file |
diff |
annotate
|
| Thu, 07 Apr 2011 12:16:27 +0200 |
blanchet |
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
|
file |
diff |
annotate
|
| Thu, 07 Apr 2011 12:16:26 +0200 |
blanchet |
make new Skolemizer more robust
|
file |
diff |
annotate
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
clean up new Skolemizer code -- some old hacks are no longer necessary
|
file |
diff |
annotate
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
remove newly added wrong logic
|
file |
diff |
annotate
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
avoid evil "export_without_context", which breaks if there are local "fixes"
|
file |
diff |
annotate
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
more robust handling of variables in new Skolemizer
|
file |
diff |
annotate
|
| Mon, 10 Jan 2011 15:45:46 +0100 |
wenzelm |
eliminated Int.toString;
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
remove at most one double negation -- any other double negations are part of some higher-order reasoning and should be left alone, cf. "HO_Reas.thy"
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
added Sledgehammer support for higher-order propositional reasoning
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
add Metis support for higher-order propositional reasoning
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
tuning: unused var
|
file |
diff |
annotate
|
| Thu, 02 Dec 2010 14:56:16 +0100 |
blanchet |
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 22:36:24 +0100 |
blanchet |
renamed "trace_me{son,tis}" and "verbose_metis" to have the name of the tool first
|
file |
diff |
annotate
|
| Tue, 23 Nov 2010 18:26:56 +0100 |
blanchet |
added "verbose" option to Metis to shut up its warnings if necessary
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 12:49:05 +0200 |
blanchet |
fixed order of quantifier instantiation in new Skolemizer
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 12:49:05 +0200 |
blanchet |
more work on new Skolemizer without Hilbert_Choice
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 12:49:05 +0200 |
blanchet |
prevent type errors because of inconsistent skolem Var types by giving fresh indices to Skolems
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 12:49:05 +0200 |
blanchet |
make handling of parameters more robust, by querying the goal
|
file |
diff |
annotate
|
| Wed, 27 Oct 2010 16:32:13 +0200 |
blanchet |
do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 11:11:23 +0200 |
blanchet |
clearer error messages
|
file |
diff |
annotate
|
| Mon, 11 Oct 2010 18:02:14 +0700 |
blanchet |
added "trace_metis" configuration option, replacing old-fashioned references
|
file |
diff |
annotate
|
| Wed, 06 Oct 2010 17:56:41 +0200 |
blanchet |
move code from "Metis_Tactics" to "Metis_Reconstruct"
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 12:50:45 +0200 |
blanchet |
tuned comments
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 11:45:10 +0200 |
blanchet |
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 22:45:09 +0200 |
blanchet |
move Metis into Plain
|
file |
diff |
annotate
| base
|