| changeset 78800 | 0b3700d31758 |
| parent 78026 | af3f1a4ba6e4 |
| 78799:807b249f1061 | 78800:0b3700d31758 |
|---|---|
4 Custom rules for Z3 proof replay. |
4 Custom rules for Z3 proof replay. |
5 *) |
5 *) |
6 |
6 |
7 signature Z3_REPLAY_RULES = |
7 signature Z3_REPLAY_RULES = |
8 sig |
8 sig |
9 val apply: Proof.context -> cterm -> thm option |
9 val apply: Simplifier.proc |
10 end; |
10 end; |
11 |
11 |
12 structure Z3_Replay_Rules: Z3_REPLAY_RULES = |
12 structure Z3_Replay_Rules: Z3_REPLAY_RULES = |
13 struct |
13 struct |
14 |
14 |