--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jun 29 10:25:53 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jun 29 10:36:36 2010 +0200
@@ -33,8 +33,8 @@
axiom_clauses: ((string * int) * thm) list option,
filtered_clauses: ((string * int) * thm) list option}
datatype failure =
- Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
- MalformedInput | MalformedOutput | UnknownError
+ Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
+ OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError
type prover_result =
{outcome: failure option,
message: string,
@@ -102,8 +102,8 @@
filtered_clauses: ((string * int) * thm) list option}
datatype failure =
- Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
- MalformedInput | MalformedOutput | UnknownError
+ Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
+ OldSpass | MalformedInput | MalformedOutput | UnknownError
type prover_result =
{outcome: failure option,