changeset 50866 | e12ebcb859a7 |
parent 50749 | 82dee320d340 |
child 50876 | e6317e8b11db |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun Jan 13 21:14:49 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun Jan 13 21:42:38 2013 +0100 @@ -244,7 +244,7 @@ (if null facts then "Found no relevant facts." else - "Including (up to) " ^ string_of_int (length facts) ^ + "Including " ^ string_of_int (length facts) ^ " relevant fact" ^ plural_s (length facts) ^ ":\n" ^ (facts |> map (fst o fst) |> space_implode " ") ^ ".") |> print