Thu, 15 Dec 2011 10:38:50 +0100 |
blanchet |
made SML/NJ happier
|
file |
diff |
annotate
|
Wed, 14 Dec 2011 23:08:03 +0100 |
blanchet |
killed dead code
|
file |
diff |
annotate
|
Wed, 14 Dec 2011 23:08:03 +0100 |
blanchet |
use new redirection algorithm in Sledgehammer
|
file |
diff |
annotate
|
Fri, 02 Dec 2011 14:54:25 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
Sat, 19 Nov 2011 12:42:21 +0100 |
blanchet |
made SML/NJ happy
|
file |
diff |
annotate
|
Fri, 18 Nov 2011 16:42:31 +0100 |
blanchet |
gave SML/NJ a chance
|
file |
diff |
annotate
|
Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
don't pass "lam_lifted" option to "metis" unless there's a good reason
|
file |
diff |
annotate
|
Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
no needless reconstructors
|
file |
diff |
annotate
|
Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
removed more clutter
|
file |
diff |
annotate
|
Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
removed needless baggage
|
file |
diff |
annotate
|
Wed, 16 Nov 2011 17:19:08 +0100 |
blanchet |
compile
|
file |
diff |
annotate
|
Wed, 16 Nov 2011 16:35:19 +0100 |
blanchet |
thread in additional options to minimizer
|
file |
diff |
annotate
|
Wed, 16 Nov 2011 13:22:36 +0100 |
blanchet |
make metis reconstruction handling more flexible
|
file |
diff |
annotate
|
Tue, 15 Nov 2011 22:13:39 +0100 |
blanchet |
continued implementation of lambda-lifting in Metis
|
file |
diff |
annotate
|
Sun, 06 Nov 2011 22:18:54 +0100 |
blanchet |
try "smt" as a fallback for ATPs if "metis" fails/times out
|
file |
diff |
annotate
|
Sun, 06 Nov 2011 22:18:54 +0100 |
blanchet |
more detailed preplay output
|
file |
diff |
annotate
|
Wed, 19 Oct 2011 21:40:32 +0200 |
blanchet |
cleaner LEO-II extensionality step detection
|
file |
diff |
annotate
|
Thu, 22 Sep 2011 16:30:47 +0200 |
blanchet |
better type reconstruction -- prevents ill-instantiations in proof replay
|
file |
diff |
annotate
|
Wed, 07 Sep 2011 13:50:17 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Wed, 07 Sep 2011 09:10:41 +0200 |
blanchet |
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
|
file |
diff |
annotate
|
Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
added caching for (in)finiteness checks
|
file |
diff |
annotate
|
Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone
|
file |
diff |
annotate
|
Wed, 10 Aug 2011 20:53:43 +0200 |
wenzelm |
old term operations are legacy;
|
file |
diff |
annotate
|
Thu, 28 Jul 2011 16:32:48 +0200 |
blanchet |
put parentheses around non-trivial metis call
|
file |
diff |
annotate
|
Wed, 20 Jul 2011 00:37:42 +0200 |
blanchet |
pass type arguments to lambda-lifted Frees, to account for polymorphism
|
file |
diff |
annotate
|
Sun, 17 Jul 2011 14:12:45 +0200 |
blanchet |
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
|
file |
diff |
annotate
|
Tue, 05 Jul 2011 17:09:59 +0100 |
nik |
improved translation of lambdas in THF
|
file |
diff |
annotate
|
Mon, 20 Jun 2011 12:13:43 +0200 |
blanchet |
clean up SPASS FLOTTER hack
|
file |
diff |
annotate
|
Thu, 16 Jun 2011 13:50:35 +0200 |
blanchet |
fixed soundness bug related to extensionality
|
file |
diff |
annotate
|
Thu, 09 Jun 2011 00:16:28 +0200 |
blanchet |
cleaner fact freshening, which also works in corner cases, e.g. if two backquoted facts have the same name (but have different variable indices)
|
file |
diff |
annotate
|
Thu, 09 Jun 2011 00:16:28 +0200 |
blanchet |
improve sort inference in Metis proofs -- in some rare cases Metis steals Isabelle's variable names and the sorts must then be inferred as well
|
file |
diff |
annotate
|
Wed, 08 Jun 2011 17:01:07 +0200 |
blanchet |
avoid duplicate facts, which confuse the minimizer output
|
file |
diff |
annotate
|
Wed, 08 Jun 2011 16:20:18 +0200 |
blanchet |
don't generate unsound proof error for missing proofs
|
file |
diff |
annotate
|
Tue, 07 Jun 2011 11:04:17 +0200 |
blanchet |
use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
|
file |
diff |
annotate
|
Tue, 07 Jun 2011 08:52:35 +0200 |
blanchet |
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
|
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 |
remove more occurrences of "metisX", preparing for the D Day when it will silently hijack "metis" and "metisFT"
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
imported patch metis_reconstr_give_type_infer_a_chance
|
file |
diff |
annotate
|
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 reconstruction of new Skolem constants 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:35 +0200 |
blanchet |
don't throw exception on unknown constants (e.g. skolems), and give more precise type to applied functions
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
slacker version of "fastype_of", in case a function has dummy type
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
only uncombine combinators in textual Isar proofs, not in Metis
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 20:36:34 +0200 |
blanchet |
temporarily added "MetisX" as reconstructor and minimizer
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 20:36:34 +0200 |
blanchet |
show what failed to play
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 20:36:34 +0200 |
blanchet |
killed odd connectives
|
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 |
fixed interaction between type tags and hAPP in reconstruction code
|
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 |
export one more function
|
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 |
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 |
first step in sharing more code between ATP and Metis translation
|
file |
diff |
annotate
| base
|