| Mon, 03 Mar 2014 12:14:47 +0100 |
wenzelm |
test polyml-svn;
|
changeset |
files
|
| Mon, 03 Mar 2014 11:58:55 +0100 |
wenzelm |
README is optional in test compilations;
|
changeset |
files
|
| Mon, 03 Mar 2014 11:58:07 +0100 |
wenzelm |
clarified path checks: avoid crash of rendering due to spurious errors;
|
changeset |
files
|
| Mon, 03 Mar 2014 11:37:06 +0100 |
wenzelm |
more precise navigation within open files;
|
changeset |
files
|
| Mon, 03 Mar 2014 10:59:33 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 03 Mar 2014 10:41:58 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 03 Mar 2014 14:22:35 +0100 |
blanchet |
updated NEWS
|
changeset |
files
|
| Mon, 03 Mar 2014 12:58:17 +0100 |
blanchet |
guard against unsound cases that arise when people peek into 'int' and similar types that are handled specially by Nitpick
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
adapted example
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
removed obsolete, harmful step in tactic
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
removed (co)iterators from documentation
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
avoid duplicate 'disc_iff' theorems
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
life without 'metis'
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalize internals
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
optimized simple non-recursive datatypes by reusing 'case' for 'rec' constant
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
compile
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
make 'diff_iff' a simp rule if available
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
less aggressive resolving
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
repaired argument list to corecursor
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
adapted to absence of 'unfold'
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
got rid of automatically generated fold constant and theorems (to reduce overhead)
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
use same identity function for abs and rep (doesn't seem to confuse any proofs)
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
make 'typedef' optional, depending on size of original type
|
changeset |
files
|