equal
deleted
inserted
replaced
91 SOME (Prove (qs2, fix, l2, t, subproofs, ((lfs, gfs), meths))) |
91 SOME (Prove (qs2, fix, l2, t, subproofs, ((lfs, gfs), meths))) |
92 end) |
92 end) |
93 | try_merge _ _ = NONE |
93 | try_merge _ _ = NONE |
94 |
94 |
95 val compress_degree = 2 |
95 val compress_degree = 2 |
96 val merge_timeout_slack = 1.2 |
96 val merge_timeout_slack = 1.25 |
97 |
97 |
98 (* Precondition: The proof must be labeled canonically |
98 (* Precondition: The proof must be labeled canonically |
99 (cf. "Slegehammer_Proof.relabel_proof_canonically"). *) |
99 (cf. "Slegehammer_Isar_Proof.relabel_isar_proof_canonically"). *) |
100 fun compress_isar_proof compress_isar |
100 fun compress_isar_proof compress_isar |
101 ({preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data) proof = |
101 ({preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data) proof = |
102 if compress_isar <= 1.0 then |
102 if compress_isar <= 1.0 then |
103 proof |
103 proof |
104 else |
104 else |