improved warning
authorblanchet
Mon, 12 Jul 2021 16:30:16 +0200
changeset 74233 96a05b8462f9
parent 74232 34c8cf767fa3
child 74234 b304285fd800
improved warning
src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Jul 12 16:30:15 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Jul 12 16:30:16 2021 +0200
@@ -169,10 +169,10 @@
   | string_of_atp_failure ProofUnparsable =
     "The prover claims the conjecture is a theorem but provided an unparsable proof"
   | string_of_atp_failure (UnsoundProof (false, ss)) =
-    "The prover derived \"False\"" ^ from_lemmas ss ^
+    "The prover derived the lemma \"False\"" ^ from_lemmas ss ^
     "; specify a sound type encoding or omit the \"type_enc\" option"
   | string_of_atp_failure (UnsoundProof (true, ss)) =
-    "The prover derived \"False\"" ^ from_lemmas ss ^
+    "The prover derived the lemma \"False\"" ^ from_lemmas ss ^
     ", which could be due to a bug in Sledgehammer or to inconsistent axioms (including \"sorry\"s)"
   | string_of_atp_failure TimedOut = "Timed out"
   | string_of_atp_failure Inappropriate =