| Wed, 08 Feb 2012 01:49:33 +0100 | blanchet | use 'primrec' to define "rotate1", for uniformity (and to help first-order tools that rely on "Spec_Rules") | changeset | files |
| Wed, 08 Feb 2012 00:55:06 +0100 | blanchet | removed fact that confuses SPASS -- better rely on "rev_rev_ident", which is stronger and more ATP friendly | changeset | files |
| Wed, 08 Feb 2012 00:05:22 +0100 | blanchet | beware of "Bit0" and "Bit1" -- these shouldn't be blidly unfolded by SPASS, lest we get gigantic terms | changeset | files |