| Tue, 03 May 2011 14:23:40 +0200 | blanchet | reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis" | changeset | files |
| Tue, 03 May 2011 08:52:32 +0200 | blanchet | whitespace tuning | changeset | files |
| Tue, 03 May 2011 08:52:16 +0200 | blanchet | make SML/NJ happiest | changeset | files |