| Thu, 25 Aug 2011 14:25:07 +0200 |
blanchet |
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 18:05:31 +0200 |
wenzelm |
modernized signature of Term.absfree/absdummy;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 20:53:43 +0200 |
wenzelm |
old term operations are legacy;
|
file |
diff |
annotate
|
| Fri, 10 Jun 2011 17:52:09 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 23:12:02 +0200 |
wenzelm |
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 20:56:08 +0200 |
wenzelm |
clarified special incr_type_indexes;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 00:16:28 +0200 |
blanchet |
removed needless function that duplicated standard functionality, with a little unnecessary twist
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 00:16:28 +0200 |
blanchet |
removed more dead code
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 00:16:28 +0200 |
blanchet |
renamed "untyped_aconv" to distinguish it clearly from the standard "aconv_untyped"
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 22:13:49 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 16:20:18 +0200 |
blanchet |
restore comment about subtle issue
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 15:56:57 +0200 |
wenzelm |
more robust exception pattern General.Subscript;
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
removed experimental code submitted by mistake
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 10:43:18 +0200 |
blanchet |
nicely thread monomorphism verbosity in Metis and Sledgehammer
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:56:06 +0200 |
blanchet |
Metis code cleanup
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
fall back in case path finder fails -- these errors are sometimes salvageable
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
more preparations towards hijacking Metis
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
reveal Skolems in new Metis
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
properly unmangle names in path finder
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
skip "hBOOL" in new Metis path finder
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:34 +0200 |
blanchet |
added Metis examples to test the new type encodings
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:34 +0200 |
blanchet |
added support for helpers in new Metis, so far only for polymorphic type encodings
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
implemented missing hAPP and ti cases of new path finder
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
tuned names
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
fixed new path finder for type information tag
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
use ":" for type information (looks good in Metis's output) and handle it in new path finder
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
tuned name
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
fixed recursive call in new path finder and (untested:) handle hAPP
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
more robust and simpler adjustment computation
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
more work on new Metis
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
more work on new metis that exploits the powerful new type encodings
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
first step in sharing more code between ATP and Metis translation
|
file |
diff |
annotate
|
| Tue, 03 May 2011 14:23:40 +0200 |
blanchet |
reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
|
file |
diff |
annotate
|
| Mon, 02 May 2011 16:33:21 +0200 |
wenzelm |
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:25 +0200 |
blanchet |
cleanup proxification/unproxification and make sure that "num_atp_type_args" is called on the proxy in the reconstruction code, since "c_fequal" has one type arg but the unproxified equal has 0
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 18:11:20 +0200 |
wenzelm |
eliminated old List.nth;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Thu, 14 Apr 2011 11:24:05 +0200 |
blanchet |
nicer error message from Metis for know failure that isn't the user's fault
|
file |
diff |
annotate
|
| Thu, 14 Apr 2011 11:24:05 +0200 |
blanchet |
make 48170228f562 work also with "HO_Reas" examples
|
file |
diff |
annotate
|
| Thu, 14 Apr 2011 11:24:05 +0200 |
blanchet |
improve on 0b05cc14c2cb: make sure that a literal variable "?foo" isn't accidentally renamed "?Q", which might be enough to confuse the new Skolemizer (cf. "Clausify.thy" example)
|
file |
diff |
annotate
|
| 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
|