Fri, 08 Aug 2014 08:26:32 +0200 |
nipkow |
tuned
|
changeset |
files
|
Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
|
changeset |
files
|
Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
generate nicer 'set' theorems for (co)datatypes
|
changeset |
files
|
Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
compile
|
changeset |
files
|
Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
took out test driver
|
changeset |
files
|
Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
make TPTP tools work on polymorphic (TFF1) problems as well
|
changeset |
files
|
Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
put comments between TPTP lines to comply with TPTP BNF
|
changeset |
files
|
Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
test driver
|
changeset |
files
|
Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
treat variables as frees in 'conjecture's
|
changeset |
files
|
Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
support TFF1 in TPTP parser/interpreter
|
changeset |
files
|
Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
tuning
|
changeset |
files
|
Thu, 07 Aug 2014 09:35:31 +0200 |
traytel |
tuned
|
changeset |
files
|
Thu, 07 Aug 2014 10:06:18 +0200 |
nipkow |
tuned
|
changeset |
files
|
Thu, 07 Aug 2014 09:48:04 +0200 |
nipkow |
tuned
|
changeset |
files
|