equal
deleted
inserted
replaced
5 Preplaying of Isar proofs. |
5 Preplaying of Isar proofs. |
6 *) |
6 *) |
7 |
7 |
8 signature SLEDGEHAMMER_ISAR_PREPLAY = |
8 signature SLEDGEHAMMER_ISAR_PREPLAY = |
9 sig |
9 sig |
10 type play_outcome = Sledgehammer_Reconstructor.play_outcome |
10 type play_outcome = Sledgehammer_Proof_Methods.play_outcome |
11 type proof_method = Sledgehammer_Isar_Proof.proof_method |
11 type proof_method = Sledgehammer_Isar_Proof.proof_method |
12 type isar_step = Sledgehammer_Isar_Proof.isar_step |
12 type isar_step = Sledgehammer_Isar_Proof.isar_step |
13 type isar_proof = Sledgehammer_Isar_Proof.isar_proof |
13 type isar_proof = Sledgehammer_Isar_Proof.isar_proof |
14 type label = Sledgehammer_Isar_Proof.label |
14 type label = Sledgehammer_Isar_Proof.label |
15 |
15 |
34 structure Sledgehammer_Isar_Preplay : SLEDGEHAMMER_ISAR_PREPLAY = |
34 structure Sledgehammer_Isar_Preplay : SLEDGEHAMMER_ISAR_PREPLAY = |
35 struct |
35 struct |
36 |
36 |
37 open ATP_Proof_Reconstruct |
37 open ATP_Proof_Reconstruct |
38 open Sledgehammer_Util |
38 open Sledgehammer_Util |
39 open Sledgehammer_Reconstructor |
39 open Sledgehammer_Proof_Methods |
40 open Sledgehammer_Isar_Proof |
40 open Sledgehammer_Isar_Proof |
41 |
41 |
42 val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false) |
42 val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false) |
43 |
43 |
44 fun enrich_context_with_local_facts proof ctxt = |
44 fun enrich_context_with_local_facts proof ctxt = |