| Sun, 29 May 2011 19:40:56 +0200 | blanchet | always check plain "metis" even if the ATP proof seems to require "metisFT" -- maybe the proof is needlessly complicated | changeset | files |
| Sun, 29 May 2011 19:40:56 +0200 | blanchet | normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages | changeset | files |
| Fri, 27 May 2011 21:11:44 +0200 | krauss | function tutorial: do not omit termination proof, even when discussing other things | changeset | files |