| Mon, 30 May 2011 12:15:17 +0100 | paulson | Fix to exception THM 1 raised (line 212 of conv.ML), reported by Andreas Lochbihler | changeset | files |
| 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 |