| Thu, 20 Feb 2014 10:32:09 +0100 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 20 Feb 2014 15:14:37 +0100 |
noschinl |
less flex-flex pairs
|
changeset |
files
|
| Thu, 20 Feb 2014 13:53:26 +0100 |
traytel |
less flex-flex pairs (thanks to Lars' statistics)
|
changeset |
files
|
| Thu, 20 Feb 2014 11:40:03 +0100 |
traytel |
made tactics more robust
|
changeset |
files
|
| Wed, 19 Feb 2014 22:08:47 +0100 |
haftmann |
offical tool
|
changeset |
files
|
| Wed, 19 Feb 2014 22:05:15 +0100 |
haftmann |
more convenient syntax for permanent interpretation
|
changeset |
files
|
| Wed, 19 Feb 2014 22:05:05 +0100 |
haftmann |
aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
|
changeset |
files
|
| Thu, 20 Feb 2014 12:27:51 +1100 |
kleing |
move stronger rules into exercise
|
changeset |
files
|
| Wed, 19 Feb 2014 15:57:02 +0000 |
sultana |
added a function that carries out all the reconstruction steps, for improved usability;
|
changeset |
files
|
| Wed, 19 Feb 2014 15:57:02 +0000 |
sultana |
reconstruction framework for LEO-II's TPTP proofs;
|
changeset |
files
|
| Wed, 19 Feb 2014 15:57:02 +0000 |
sultana |
made list of test files a parameter to timed_test in TPTP_Test.thy, and updated dependent definitions;
|
changeset |
files
|
| Wed, 19 Feb 2014 15:57:02 +0000 |
sultana |
cleaned code used to produce a proof-graph;
|
changeset |
files
|