| 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
|
| Mon, 03 Mar 2014 12:48:19 +0100 |
blanchet |
use aconv to compare terms (for cleanliness)
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:19 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:19 +0100 |
blanchet |
optimize cardinal bounds involving natLeq (omega)
|
changeset |
files
|
| Mon, 03 Mar 2014 03:13:45 +0100 |
wenzelm |
no extend_word for now, it is in conflict with manual reformatting of sources via TAB (e.g. accidental replacement of 'assume' by 'assumes');
|
changeset |
files
|
| Sun, 02 Mar 2014 22:43:20 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 02 Mar 2014 22:39:34 +0100 |
wenzelm |
more standard module name;
|
changeset |
files
|