src/HOL/Tools/ATP/atp_util.ML
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