| Thu, 10 May 2012 21:02:36 +0200 |
huffman |
simplify instance proofs for rat
|
changeset |
files
|
| Thu, 10 May 2012 21:18:41 +0200 |
huffman |
convert Rat.thy to use lift_definition/transfer
|
changeset |
files
|
| Thu, 10 May 2012 16:56:23 +0200 |
blanchet |
cleaner handling of bi-implication for THF output of first-order type encodings
|
changeset |
files
|
| Thu, 10 May 2012 16:56:23 +0200 |
blanchet |
distinguish between instantiated and uninstantiated inductions -- the latter are OK for first-order provers
|
changeset |
files
|
| Thu, 10 May 2012 12:23:20 +0200 |
huffman |
temporarily comment out broken nitpick example
|
changeset |
files
|
| Thu, 10 May 2012 09:10:43 +0200 |
huffman |
convert real number theory to use lifting/transfer
|
changeset |
files
|
| Mon, 07 May 2012 15:04:17 +0200 |
huffman |
tuned ordering of lemmas
|
changeset |
files
|
| Thu, 10 May 2012 10:07:41 +0200 |
blanchet |
pass fewer facts to LEO-II and Satallax
|
changeset |
files
|
| Thu, 10 May 2012 10:07:40 +0200 |
blanchet |
tweak LEO-II setup
|
changeset |
files
|
| Thu, 10 May 2012 10:07:40 +0200 |
blanchet |
use raw monomorphic encoding with Waldmeister, to avoid overloading it with too many function symbols (as would be the case using mangled monomorphic encodings)
|
changeset |
files
|
| Wed, 09 May 2012 11:24:38 +0200 |
bulwahn |
build Pure_64 with new settings
|
changeset |
files
|
| Wed, 09 May 2012 11:17:54 +0200 |
bulwahn |
tuned
|
changeset |
files
|
| Wed, 09 May 2012 10:39:54 +0200 |
bulwahn |
playing around with mira settings
|
changeset |
files
|
| Tue, 08 May 2012 14:35:13 +0200 |
bulwahn |
defining and proving Executable_Relation with lift_definition and transfer
|
changeset |
files
|
| Tue, 08 May 2012 14:31:03 +0200 |
bulwahn |
specialised fact in the Record theory should not be appear in proofs discovered by sledgehammer
|
changeset |
files
|