| 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
|
| Sun, 02 Mar 2014 22:37:55 +0100 |
wenzelm |
silence warning due to addsimps @{thms dnf_simps}: duplicate not_not rule via simp_thms and nnf_simps;
|
changeset |
files
|
| Sun, 02 Mar 2014 22:24:52 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Sun, 02 Mar 2014 22:03:27 +0100 |
wenzelm |
allow suffix of underscores (usually unused names), to extend completion beyond already recognized entry;
|
changeset |
files
|
| Sun, 02 Mar 2014 21:52:44 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|