| Thu, 16 Jun 2011 13:50:35 +0200 | blanchet | gave up an optimization that sometimes lead to unsound proofs -- in short, facts talking about a schematic type variable can encode a cardinality constraint and be consistent with HOL, e.g. "card (UNIV::?'a set) = 1 ==> ALL x y. x = y" | file | diff | annotate |
| Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | gracefully handle the case where a constant is partially or not instantiated at all, as may happen when reconstructing Metis proofs for polymorphic type encodings | file | diff | annotate |
| Tue, 31 May 2011 16:38:36 +0200 | blanchet | first step in sharing more code between ATP and Metis translation | file | diff | annotate |