| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
always use DFG format to talk to SPASS -- since that's what we'll need to use anyway to benefit from sorts and other extensions
|
changeset |
files
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
added DFG unsorted support (like in the old days)
|
changeset |
files
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
gracefully do nothing if the SPASS input file is already in DFG format
|
changeset |
files
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
added sorted DFG output for coming version of SPASS
|
changeset |
files
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
specify proof output level 1 (i.e. no detailed, potentially huge E proofs) to LEO-II; requires version 1.2.9
|
changeset |
files
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
check "sound" flag before doing something unsound...
|
changeset |
files
|
| Sat, 29 Oct 2011 12:57:43 +0200 |
wenzelm |
uniform treatment of syntax declaration wrt. aux. context (NB: notation avoids duplicate mixfix internally);
|
changeset |
files
|
| Sat, 29 Oct 2011 12:55:34 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 28 Oct 2011 16:49:15 +0200 |
huffman |
more accurate class constraints on cancellation simproc patterns
|
changeset |
files
|
| Sat, 29 Oct 2011 00:23:58 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 28 Oct 2011 23:41:16 +0200 |
wenzelm |
tuned Named_Thms: proper binding;
|
changeset |
files
|
| Fri, 28 Oct 2011 23:16:50 +0200 |
wenzelm |
refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;
|
changeset |
files
|
| Fri, 28 Oct 2011 23:10:44 +0200 |
wenzelm |
more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
|
changeset |
files
|
| Fri, 28 Oct 2011 22:17:30 +0200 |
wenzelm |
uniform Local_Theory.declaration with explicit params;
|
changeset |
files
|
| Fri, 28 Oct 2011 17:15:52 +0200 |
wenzelm |
tuned signature -- refined terminology;
|
changeset |
files
|