blanchet [Mon, 03 Mar 2014 12:48:20 +0100] rev 57199
adapted to absence of 'unfold'
blanchet [Mon, 03 Mar 2014 12:48:20 +0100] rev 57198
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet [Mon, 03 Mar 2014 12:48:20 +0100] rev 57197
use same identity function for abs and rep (doesn't seem to confuse any proofs)
blanchet [Mon, 03 Mar 2014 12:48:20 +0100] rev 57196
make 'typedef' optional, depending on size of original type
blanchet [Mon, 03 Mar 2014 12:48:19 +0100] rev 57195
use aconv to compare terms (for cleanliness)
blanchet [Mon, 03 Mar 2014 12:48:19 +0100] rev 57194
tuning
blanchet [Mon, 03 Mar 2014 12:48:19 +0100] rev 57193
optimize cardinal bounds involving natLeq (omega)
wenzelm [Mon, 03 Mar 2014 03:13:45 +0100] rev 57192
no extend_word for now, it is in conflict with manual reformatting of sources via TAB (e.g. accidental replacement of 'assume' by 'assumes');
wenzelm [Sun, 02 Mar 2014 22:43:20 +0100] rev 57191
merged
wenzelm [Sun, 02 Mar 2014 22:39:34 +0100] rev 57190
more standard module name;