| Mon, 29 Jul 2013 18:06:39 +0200 |
blanchet |
avoid duplicating Var when the types do not quite fit -- since this step occurs before type inference
|
file |
diff |
annotate
|
| Fri, 24 May 2013 16:43:37 +0200 |
blanchet |
improved handling of free variables' types in Isar proofs
|
file |
diff |
annotate
|
| Thu, 16 May 2013 14:58:30 +0200 |
blanchet |
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
|
file |
diff |
annotate
|
| Thu, 16 May 2013 13:34:13 +0200 |
blanchet |
tuning -- renamed '_from_' to '_of_' in Sledgehammer
|
file |
diff |
annotate
|
| Mon, 06 May 2013 11:03:08 +0200 |
smolkas |
handle dummy atp terms
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 08:44:24 +0100 |
blanchet |
slacker comparison for Skolems, to avoid trivial equations
|
file |
diff |
annotate
|
| Thu, 03 Jan 2013 17:10:12 +0100 |
blanchet |
rename variable in binder, not just in body
|
file |
diff |
annotate
|
| Thu, 03 Jan 2013 15:13:11 +0100 |
blanchet |
swap Vampire's Skolem arguments to bring them in line with what E and metis's new skolemizer do (helps Isar proof reconstruction in some cases)
|
file |
diff |
annotate
|
| Thu, 03 Jan 2013 00:02:15 +0100 |
blanchet |
tuned comment
|
file |
diff |
annotate
|
| Wed, 02 Jan 2013 19:59:06 +0100 |
blanchet |
generate "obtain" steps corresponding to skolemization inferences
|
file |
diff |
annotate
|
| Wed, 02 Jan 2013 13:14:47 +0100 |
blanchet |
properly take the existential closure of skolems
|
file |
diff |
annotate
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
use metaquantification when possible in Isar proofs
|
file |
diff |
annotate
|
| Thu, 18 Oct 2012 13:19:44 +0200 |
blanchet |
refactor code
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 18:50:53 +0200 |
blanchet |
added proof minimization code from Steffen Smolka
|
file |
diff |
annotate
|
| Tue, 09 Oct 2012 00:40:33 +0200 |
blanchet |
added type annotations to generated Isar proofs -- code by Steffen Smolka
|
file |
diff |
annotate
|