| Wed, 05 Feb 2014 09:25:48 +0100 |
blanchet |
got rid of indices
|
changeset |
files
|
| Wed, 05 Feb 2014 09:07:08 +0100 |
blanchet |
corrected wrong 'meth :: _' pattern maching + tuned code
|
changeset |
files
|
| Tue, 04 Feb 2014 23:11:18 +0100 |
blanchet |
more generous Isar proof compression -- try to remove failing steps
|
changeset |
files
|
| Tue, 04 Feb 2014 23:11:18 +0100 |
blanchet |
tweaked handling of 'hopeless' methods
|
changeset |
files
|
| Tue, 04 Feb 2014 23:11:18 +0100 |
blanchet |
do a second phase of proof compression after minimization
|
changeset |
files
|
| Tue, 04 Feb 2014 23:11:18 +0100 |
blanchet |
don't give up on hopeless proof methods -- they can become hopeful again
|
changeset |
files
|
| Tue, 04 Feb 2014 23:11:18 +0100 |
blanchet |
tuned code
|
changeset |
files
|
| Tue, 04 Feb 2014 23:11:18 +0100 |
blanchet |
tuned slack
|
changeset |
files
|
| Tue, 04 Feb 2014 23:11:18 +0100 |
blanchet |
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
|
changeset |
files
|
| Tue, 04 Feb 2014 21:29:46 +0000 |
paulson |
removal of "back", etc.
|
changeset |
files
|
| Tue, 04 Feb 2014 21:28:38 +0000 |
paulson |
Restoration of Pocklington.thy. Tidying.
|
changeset |
files
|
| Tue, 04 Feb 2014 21:01:35 +0100 |
nipkow |
tuned latex
|
changeset |
files
|
| Tue, 04 Feb 2014 17:59:33 +0100 |
nipkow |
tuned latex
|
changeset |
files
|
| Tue, 04 Feb 2014 17:44:15 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Tue, 04 Feb 2014 17:38:54 +0100 |
nipkow |
started index
|
changeset |
files
|