--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Jun 28 18:47:07 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jun 29 09:05:37 2010 +0200
@@ -48,6 +48,7 @@
filtered_clauses: ((string * int) * thm) list}
type prover =
params -> minimize_command -> Time.time -> problem -> prover_result
+ exception TRIVIAL of unit
val kill_atps: unit -> unit
val running_atps: unit -> unit
@@ -119,6 +120,9 @@
type prover =
params -> minimize_command -> Time.time -> problem -> prover_result
+(* Trivial problem, which resolution cannot handle (empty clause) *)
+exception TRIVIAL of unit
+
(* named provers *)
structure Data = Theory_Data