| Tue, 22 May 2012 16:59:27 +0200 | blanchet | make higher-order goals more first-order via extensionality | changeset | files |
| Tue, 22 May 2012 16:59:27 +0200 | blanchet | added "ext_cong_neq" lemma (not used yet); tuning | changeset | files |
| Mon, 21 May 2012 16:37:28 +0200 | kuncar | use quot_del instead of ML code in Rat.thy | changeset | files |
| Mon, 21 May 2012 16:36:48 +0200 | kuncar | quot_del attribute, it allows us to deregister quotient types | changeset | files |
| Mon, 21 May 2012 11:31:52 +0200 | blanchet | invite users to upgrade their SPASS (so we can get rid of old code) | changeset | files |
| Mon, 21 May 2012 11:31:52 +0200 | blanchet | start phasing out old SPASS | changeset | files |
| Mon, 21 May 2012 11:31:52 +0200 | blanchet | minor tweak in Vampire setup | changeset | files |