Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
make "metisX"'s default more like old "metis"
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
fixed type helper indices in new Metis
|
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:34 +0200 |
blanchet |
use "metisX" as fallback, since it's much faster than "metisFT"
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 20:36:34 +0200 |
blanchet |
clean up unnecessary machinery -- helpers work also with monomorphic 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 |
fixed Isabelle version of lightweight tag theorem, using "Thm.trivial" not "Thm.assume"
|
file |
diff |
annotate
|
Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
support lightweight tags in new Metis
|
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 |
tuned name
|
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 |
parse optional type system specification
|
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
|
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 |
tuning
|
file |
diff |
annotate
|
Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
removed obscure option
|
file |
diff |
annotate
|
Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
added "metisX" syntax (temporary)
|
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
|
Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
|
file |
diff |
annotate
|
Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
try both "metis" and (on failure) "metisFT" in replay
|
file |
diff |
annotate
|
Thu, 19 May 2011 10:24:13 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
|
file |
diff |
annotate
|
Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
added unfold set constant functionality to Meson/Metis -- disabled by default for now
|
file |
diff |
annotate
|
Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
more robust exception handling in Metis (also works if there are several subgoals)
|
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
|