changeset 37616 | c8d2d84d6011 |
parent 37578 | 9367cb36b1c4 |
child 37624 | 3ee568334813 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Jun 28 13:36:21 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Jun 28 17:31:38 2010 +0200 @@ -30,6 +30,7 @@ open Clausifier open Metis_Clauses open Sledgehammer_Util +open Sledgehammer_Fact_Filter type minimize_command = string list -> string