author | blanchet |
Sat, 05 Jan 2013 22:31:33 +0100 | |
changeset 50751 | d3111134973d |
parent 50750 | 518f0b5ef3d9 |
child 50752 | d5834be31864 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Jan 05 22:31:32 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Jan 05 22:31:33 2013 +0100 @@ -866,7 +866,7 @@ " proofs to learn." ^ (if auto_level = 0 andalso not run_prover then "\n\nHint: Try " ^ sendback learn_proverN ^ - " to learn from automatic provers." + " to learn from an automatic prover." else "") else