2011-08-25 blanchet 2011-08-25 make default unsound mode less unsound
2011-08-25 blanchet 2011-08-25 fixed bang encoding detection of which types to encode
2011-08-24 blanchet 2011-08-24 tuning
2011-08-22 blanchet 2011-08-22 added caching for (in)finiteness checks
2011-08-22 blanchet 2011-08-22 make sound mode more sound (and clean up code)
2011-08-22 blanchet 2011-08-22 reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
2011-07-17 blanchet 2011-07-17 fixed lambda-liftg: must ensure the formulas are in close form
2011-07-17 blanchet 2011-07-17 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
2011-07-14 blanchet 2011-07-14 added option to control which lambda translation to use (for experiments)
2011-06-27 blanchet 2011-06-27 added "sound" option to force Sledgehammer to be pedantically sound
2011-06-16 blanchet 2011-06-16 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"
2011-06-06 blanchet 2011-06-06 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
2011-05-31 blanchet 2011-05-31 first step in sharing more code between ATP and Metis translation