| Sat, 09 Aug 2014 21:03:42 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 05 Aug 2014 10:59:40 +0200 |
blanchet |
rationalize Skolem names
|
file |
diff |
annotate
|
| Tue, 05 Aug 2014 10:02:35 +0200 |
blanchet |
tuned code
|
file |
diff |
annotate
|
| Tue, 05 Aug 2014 09:58:23 +0200 |
blanchet |
don't rename variables which will be renamed later anyway
|
file |
diff |
annotate
|
| Tue, 05 Aug 2014 09:55:42 +0200 |
blanchet |
normalize skolem argument variable names so that they coincide when taking the conjunction
|
file |
diff |
annotate
|
| Tue, 05 Aug 2014 09:20:00 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 04 Aug 2014 16:53:09 +0200 |
blanchet |
deal with E definitions
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 23:29:50 +0200 |
blanchet |
fine-tuned Isar reconstruction, esp. boolean simplifications
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 23:29:49 +0200 |
blanchet |
centralized boolean simplification so that e.g. LEO-II benefits from it
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 20:44:29 +0200 |
blanchet |
better handling of variable names
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 23:52:56 +0200 |
blanchet |
unlift before uncombine, because the definition of a lambda-lifted symbol might have an SK combinator in it (in hybrid encodings)
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:13 +0200 |
fleury |
Whitespace and indentation correction.
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
imported patch hilbert_choice_support
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
imported patch satallax_proof_support_Sledgehammer
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:11 +0200 |
fleury |
removing the '= True' generated by Leo-II.
|
file |
diff |
annotate
|