--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Jun 28 18:15:40 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Jun 28 18:46:42 2010 +0200
@@ -8,7 +8,6 @@
signature ATP_MANAGER =
sig
- type cnf_thm = Clausifier.cnf_thm
type name_pool = Metis_Clauses.name_pool
type relevance_override = Sledgehammer_Fact_Filter.relevance_override
type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
@@ -31,8 +30,8 @@
{subgoal: int,
goal: Proof.context * (thm list * thm),
relevance_override: relevance_override,
- axiom_clauses: cnf_thm list option,
- filtered_clauses: cnf_thm list option}
+ axiom_clauses: ((string * int) * thm) list option,
+ filtered_clauses: ((string * int) * thm) list option}
datatype failure =
Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
MalformedInput | MalformedOutput | UnknownError
@@ -46,7 +45,7 @@
proof: string,
internal_thm_names: string Vector.vector,
conjecture_shape: int list list,
- filtered_clauses: cnf_thm list}
+ filtered_clauses: ((string * int) * thm) list}
type prover =
params -> minimize_command -> Time.time -> problem -> prover_result
@@ -98,8 +97,8 @@
{subgoal: int,
goal: Proof.context * (thm list * thm),
relevance_override: relevance_override,
- axiom_clauses: cnf_thm list option,
- filtered_clauses: cnf_thm list option}
+ axiom_clauses: ((string * int) * thm) list option,
+ filtered_clauses: ((string * int) * thm) list option}
datatype failure =
Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
@@ -115,7 +114,7 @@
proof: string,
internal_thm_names: string Vector.vector,
conjecture_shape: int list list,
- filtered_clauses: cnf_thm list}
+ filtered_clauses: ((string * int) * thm) list}
type prover =
params -> minimize_command -> Time.time -> problem -> prover_result