| changeset 41114 | f9ae7c2abf7e |
| parent 40317 | 1eac228c52b3 |
| child 41493 | f05976d69141 |
| 41113:b223fa19af3c | 41114:f9ae7c2abf7e |
|---|---|
1 (* Title: HOL/Tools/Function/scnp_reconstruct.ML |
1 (* Title: HOL/Tools/Function/scnp_reconstruct.ML |
2 Author: Armin Heller, TU Muenchen |
2 Author: Armin Heller, TU Muenchen |
3 Author: Alexander Krauss, TU Muenchen |
3 Author: Alexander Krauss, TU Muenchen |
4 |
4 |
5 Proof reconstruction for SCNP |
5 Proof reconstruction for SCNP termination. |
6 *) |
6 *) |
7 |
7 |
8 signature SCNP_RECONSTRUCT = |
8 signature SCNP_RECONSTRUCT = |
9 sig |
9 sig |
10 |
10 |