equal
deleted
inserted
replaced
9 sig |
9 sig |
10 type atp_step_name = ATP_Proof.atp_step_name |
10 type atp_step_name = ATP_Proof.atp_step_name |
11 type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step |
11 type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step |
12 type 'a atp_proof = 'a ATP_Proof.atp_proof |
12 type 'a atp_proof = 'a ATP_Proof.atp_proof |
13 type stature = ATP_Problem_Generate.stature |
13 type stature = ATP_Problem_Generate.stature |
14 type one_line_params = Sledgehammer_Reconstructor.one_line_params |
14 type one_line_params = Sledgehammer_Proof_Methods.one_line_params |
15 |
15 |
16 val trace : bool Config.T |
16 val trace : bool Config.T |
17 |
17 |
18 type isar_params = |
18 type isar_params = |
19 bool * (string option * string option) * Time.time * real * bool * bool |
19 bool * (string option * string option) * Time.time * real * bool * bool |
29 open ATP_Util |
29 open ATP_Util |
30 open ATP_Problem |
30 open ATP_Problem |
31 open ATP_Proof |
31 open ATP_Proof |
32 open ATP_Proof_Reconstruct |
32 open ATP_Proof_Reconstruct |
33 open Sledgehammer_Util |
33 open Sledgehammer_Util |
34 open Sledgehammer_Reconstructor |
34 open Sledgehammer_Proof_Methods |
35 open Sledgehammer_Isar_Proof |
35 open Sledgehammer_Isar_Proof |
36 open Sledgehammer_Isar_Preplay |
36 open Sledgehammer_Isar_Preplay |
37 open Sledgehammer_Isar_Compress |
37 open Sledgehammer_Isar_Compress |
38 open Sledgehammer_Isar_Minimize |
38 open Sledgehammer_Isar_Minimize |
39 |
39 |