changeset 43037 | ade5c84f860f |
parent 43027 | b10775a669d1 |
child 43043 | 1406f6fc5dc3 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri May 27 10:30:08 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri May 27 10:30:08 2011 +0200 @@ -61,7 +61,7 @@ (if blocking then "." else - ":\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))) + "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))) val auto_minimize_min_facts = Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}