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
|