111 "The prover claims the conjecture is a theorem but did not provide a proof." |
111 "The prover claims the conjecture is a theorem but did not provide a proof." |
112 | string_for_failure ProofIncomplete = |
112 | string_for_failure ProofIncomplete = |
113 "The prover claims the conjecture is a theorem but provided an incomplete \ |
113 "The prover claims the conjecture is a theorem but provided an incomplete \ |
114 \(or unparsable) proof." |
114 \(or unparsable) proof." |
115 | string_for_failure (UnsoundProof (false, ss)) = |
115 | string_for_failure (UnsoundProof (false, ss)) = |
116 "The prover found a type-unsound proof " ^ involving ss ^ |
116 "The prover found an unsound proof " ^ involving ss ^ |
117 "(or, less likely, your axioms are inconsistent). Specify a sound type \ |
117 "(or, less likely, your axioms are inconsistent). Specify a sound type \ |
118 \encoding or omit the \"type_enc\" option." |
118 \encoding or omit the \"type_enc\" option." |
119 | string_for_failure (UnsoundProof (true, ss)) = |
119 | string_for_failure (UnsoundProof (true, ss)) = |
120 "The prover found a type-unsound proof " ^ involving ss ^ |
120 "The prover found an unsound proof " ^ involving ss ^ |
121 "even though a supposedly type-sound encoding was used (or, less likely, \ |
121 "(or, less likely, your axioms are inconsistent). Please report this to \ |
122 \your axioms are inconsistent). Please report this to the Isabelle \ |
122 \the Isabelle developers." |
123 \developers." |
|
124 | string_for_failure CantConnect = "Cannot connect to remote server." |
123 | string_for_failure CantConnect = "Cannot connect to remote server." |
125 | string_for_failure TimedOut = "Timed out." |
124 | string_for_failure TimedOut = "Timed out." |
126 | string_for_failure Inappropriate = |
125 | string_for_failure Inappropriate = |
127 "The generated problem lies outside the prover's scope." |
126 "The generated problem lies outside the prover's scope." |
128 | string_for_failure OutOfResources = "The prover ran out of resources." |
127 | string_for_failure OutOfResources = "The prover ran out of resources." |