| Thu, 19 Dec 2013 19:16:44 +0100 |
blanchet |
don't do 'isar_try0' if preplaying is off
|
file |
diff |
annotate
|
| Thu, 19 Dec 2013 18:39:54 +0100 |
blanchet |
more data structure refactoring
|
file |
diff |
annotate
|
| Thu, 19 Dec 2013 18:22:31 +0100 |
blanchet |
data structure rationalization
|
file |
diff |
annotate
|
| Mon, 16 Dec 2013 14:49:18 +0100 |
blanchet |
generalize method list further to list of list (clustering preferred methods together)
|
file |
diff |
annotate
|
| Mon, 16 Dec 2013 12:26:18 +0100 |
blanchet |
store alternative proof methods in Isar data structure
|
file |
diff |
annotate
|
| Mon, 16 Dec 2013 12:02:28 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 16 Dec 2013 09:48:26 +0100 |
blanchet |
added 'meson' to the mix
|
file |
diff |
annotate
|
| Tue, 10 Dec 2013 15:24:17 +0800 |
blanchet |
more work on Z3 Isar proofs
|
file |
diff |
annotate
|
| Mon, 09 Dec 2013 06:33:46 +0100 |
blanchet |
adapted code for Z3 proof reconstruction
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 18:38:25 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 12 Jul 2013 21:07:34 +0200 |
smolkas |
added blast, force
|
file |
diff |
annotate
|
| Fri, 12 Jul 2013 19:03:08 +0200 |
smolkas |
cleaner preplay interface
|
file |
diff |
annotate
|
| Fri, 12 Jul 2013 14:18:06 +0200 |
smolkas |
tuned
|
file |
diff |
annotate
|
| Fri, 12 Jul 2013 14:18:06 +0200 |
smolkas |
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
|
file |
diff |
annotate
|
| Thu, 11 Jul 2013 20:08:06 +0200 |
smolkas |
optimize isar-proofs by trying different proof methods
|
file |
diff |
annotate
|