equal
deleted
inserted
replaced
10 sig |
10 sig |
11 type isar_proof = Sledgehammer_Proof.isar_proof |
11 type isar_proof = Sledgehammer_Proof.isar_proof |
12 type preplay_interface = Sledgehammer_Preplay.preplay_interface |
12 type preplay_interface = Sledgehammer_Preplay.preplay_interface |
13 |
13 |
14 val try0 : Time.time -> preplay_interface -> isar_proof -> isar_proof |
14 val try0 : Time.time -> preplay_interface -> isar_proof -> isar_proof |
15 end |
15 end; |
16 |
16 |
17 structure Sledgehammer_Try0 : SLEDGEHAMMER_TRY0 = |
17 structure Sledgehammer_Try0 : SLEDGEHAMMER_TRY0 = |
18 struct |
18 struct |
19 |
19 |
20 open Sledgehammer_Proof |
20 open Sledgehammer_Proof |
57 end |
57 end |
58 |
58 |
59 fun try0 preplay_timeout preplay_interface proof = |
59 fun try0 preplay_timeout preplay_interface proof = |
60 map_isar_steps (try0_step preplay_timeout preplay_interface) proof |
60 map_isar_steps (try0_step preplay_timeout preplay_interface) proof |
61 |
61 |
62 end |
62 end; |