| Fri, 26 Feb 2010 21:43:26 +0100 |
wenzelm |
tuned hyp_subst_tac';
|
changeset |
files
|
| Fri, 26 Feb 2010 18:38:23 +0100 |
blanchet |
use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
|
changeset |
files
|
| Fri, 26 Feb 2010 16:50:09 +0100 |
blanchet |
merged
|
changeset |
files
|
| Fri, 26 Feb 2010 16:49:46 +0100 |
blanchet |
more work on the new monotonicity stuff in Nitpick
|
changeset |
files
|
| Thu, 25 Feb 2010 16:33:39 +0100 |
blanchet |
improved precision of infinite "shallow" datatypes in Nitpick;
|
changeset |
files
|
| Thu, 25 Feb 2010 10:08:44 +0100 |
blanchet |
cosmetics
|
changeset |
files
|
| Fri, 26 Feb 2010 13:29:43 +0100 |
bulwahn |
merged
|
changeset |
files
|
| Fri, 26 Feb 2010 09:49:00 +0100 |
bulwahn |
merged
|
changeset |
files
|
| Thu, 25 Feb 2010 15:36:38 +0100 |
bulwahn |
adding no_topmost_reordering as new option to the code_pred command
|
changeset |
files
|
| Thu, 25 Feb 2010 14:01:34 +0100 |
bulwahn |
adopting Mutabelle to quickcheck reporting; improving quickcheck reporting
|
changeset |
files
|
| Thu, 25 Feb 2010 10:04:50 +0100 |
bulwahn |
added quiet option to quickcheck command
|
changeset |
files
|
| Thu, 25 Feb 2010 09:28:01 +0100 |
bulwahn |
added basic reporting of test cases to quickcheck
|
changeset |
files
|
| Fri, 26 Feb 2010 10:57:35 +0100 |
haftmann |
merged
|
changeset |
files
|
| Fri, 26 Feb 2010 10:48:21 +0100 |
haftmann |
use abstract code cerficates for bare code theorems
|
changeset |
files
|
| Fri, 26 Feb 2010 10:48:20 +0100 |
haftmann |
implement quotient_of for odl SML code generator
|
changeset |
files
|