| Wed, 18 Dec 2013 16:50:14 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 16 Dec 2013 09:17:58 +0100 |
blanchet |
made SML/NJ happy
|
file |
diff |
annotate
|
| Sun, 15 Dec 2013 22:03:12 +0100 |
blanchet |
generate proper succedent for cases with trivial branches
|
file |
diff |
annotate
|
| Sun, 15 Dec 2013 18:01:38 +0100 |
blanchet |
use 'arith' when appropriate in Z3 proofs
|
file |
diff |
annotate
|
| Sun, 15 Dec 2013 18:01:38 +0100 |
blanchet |
robustness in degenerate case + tuning
|
file |
diff |
annotate
|
| Fri, 13 Dec 2013 22:54:39 +0800 |
blanchet |
made SML/NJ happy + whitespace tuning
|
file |
diff |
annotate
|
| Wed, 11 Dec 2013 22:23:07 +0800 |
blanchet |
removed inlined rewriting'' for one-branch case splits in Isar proofs, since these can yield huge unreadable formulas
|
file |
diff |
annotate
|
| Fri, 22 Feb 2013 17:02:16 +0100 |
wenzelm |
make SML/NJ happy;
|
file |
diff |
annotate
|
| Thu, 21 Feb 2013 12:22:26 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 17:05:24 +0100 |
blanchet |
remove needless steps from refutation graph -- these confuse the proof redirection algorithm (and are needless)
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 16:21:04 +0100 |
blanchet |
more precise error
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 10:00:25 +0100 |
blanchet |
tuned code
|
file |
diff |
annotate
|
| Thu, 07 Feb 2013 18:39:24 +0100 |
blanchet |
more robustness in Isar proof reconstruction (cf. bug report by Ondrej)
|
file |
diff |
annotate
|
| Thu, 07 Feb 2013 18:24:31 +0100 |
blanchet |
more precise error message
|
file |
diff |
annotate
|
| Wed, 02 Jan 2013 20:53:01 +0100 |
smolkas |
removed old, unused code
|
file |
diff |
annotate
|
| Fri, 02 Nov 2012 16:16:48 +0100 |
blanchet |
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
|
file |
diff |
annotate
|
| Wed, 16 May 2012 18:16:51 +0200 |
blanchet |
more helpful error message
|
file |
diff |
annotate
|
| Tue, 15 May 2012 13:06:15 +0200 |
blanchet |
made SML/NJ happy
|
file |
diff |
annotate
|
| Mon, 14 May 2012 15:54:26 +0200 |
blanchet |
repaired snag in debug function
|
file |
diff |
annotate
|
| Mon, 14 May 2012 15:54:26 +0200 |
blanchet |
added debugging function
|
file |
diff |
annotate
|
| Mon, 23 Jan 2012 17:40:32 +0100 |
blanchet |
renamed two files to make room for a new file
|
file |
diff |
annotate
| base
|