equal
deleted
inserted
replaced
10 val read_tptp_file : theory -> (string * term -> 'a) -> string -> |
10 val read_tptp_file : theory -> (string * term -> 'a) -> string -> |
11 'a list * ('a list * 'a list) * local_theory |
11 'a list * ('a list * 'a list) * local_theory |
12 val nitpick_tptp_file : theory -> int -> string -> unit |
12 val nitpick_tptp_file : theory -> int -> string -> unit |
13 val refute_tptp_file : theory -> int -> string -> unit |
13 val refute_tptp_file : theory -> int -> string -> unit |
14 val can_tac : Proof.context -> (Proof.context -> tactic) -> term -> bool |
14 val can_tac : Proof.context -> (Proof.context -> tactic) -> term -> bool |
15 val SOLVE_TIMEOUT : int -> string -> tactic -> tactic |
15 val SOLVE_TIMEOUT : int -> string -> tactic -> tactic |
16 val atp_tac : local_theory -> int -> (string * string) list -> int -> term list -> string -> |
16 val atp_tac : local_theory -> int -> (string * string) list -> int -> term list -> string -> |
17 int -> tactic |
17 int -> tactic |
18 val smt_solver_tac : string -> local_theory -> int -> tactic |
18 val smt_solver_tac : string -> local_theory -> int -> tactic |
19 val make_conj : term list * term list -> term list -> term |
19 val make_conj : term list * term list -> term list -> term |
20 val sledgehammer_tptp_file : theory -> int -> string -> unit |
20 val sledgehammer_tptp_file : theory -> int -> string -> unit |