equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 signature SLEDGEHAMMER_ISAR_PREPLAY = |
8 signature SLEDGEHAMMER_ISAR_PREPLAY = |
9 sig |
9 sig |
10 type play_outcome = Sledgehammer_Proof_Methods.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_Proof_Methods.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 |
16 val trace : bool Config.T |
16 val trace : bool Config.T |