equal
deleted
inserted
replaced
6 Sledgehammer's translation. |
6 Sledgehammer's translation. |
7 *) |
7 *) |
8 |
8 |
9 signature ATP_EXPORT = |
9 signature ATP_EXPORT = |
10 sig |
10 sig |
|
11 val theorems_mentioned_in_proof_term : |
|
12 string list option -> thm -> string list |
11 val generate_tptp_graph_file_for_theory : |
13 val generate_tptp_graph_file_for_theory : |
12 Proof.context -> theory -> string -> unit |
14 Proof.context -> theory -> string -> unit |
13 val generate_tptp_inference_file_for_theory : |
15 val generate_tptp_inference_file_for_theory : |
14 Proof.context -> theory -> string -> string -> unit |
16 Proof.context -> theory -> string -> string -> unit |
15 end; |
17 end; |
108 val facts0 = facts_of thy |
110 val facts0 = facts_of thy |
109 val facts = |
111 val facts = |
110 facts0 |> map (fn ((_, loc), th) => |
112 facts0 |> map (fn ((_, loc), th) => |
111 ((Thm.get_name_hint th, loc), prop_of th)) |
113 ((Thm.get_name_hint th, loc), prop_of th)) |
112 val (atp_problem, _, _, _, _, _, _) = |
114 val (atp_problem, _, _, _, _, _, _) = |
113 prepare_atp_problem ctxt format Axiom Axiom type_sys false false true [] |
115 prepare_atp_problem ctxt format Axiom Axiom type_sys true false true [] |
114 @{prop False} facts |
116 @{prop False} facts |
115 val all_names = facts0 |> map (Thm.get_name_hint o snd) |
117 val all_names = facts0 |> map (Thm.get_name_hint o snd) |
116 val infers = |
118 val infers = |
117 facts0 |> map (fn (_, th) => |
119 facts0 |> map (fn (_, th) => |
118 (fact_name_of (Thm.get_name_hint th), |
120 (fact_name_of (Thm.get_name_hint th), |