| changeset 58889 | 5b7a9633cfa8 |
| parent 55417 | 01fbfb60c33e |
| child 61076 | bdc1e2f0a86a |
| 58888:9537bf1c4853 | 58889:5b7a9633cfa8 |
|---|---|
2 Author: Jasmin Blanchette, TU Muenchen |
2 Author: Jasmin Blanchette, TU Muenchen |
3 |
3 |
4 Example that exercises Metis's Clausifier. |
4 Example that exercises Metis's Clausifier. |
5 *) |
5 *) |
6 |
6 |
7 header {* Example that Exercises Metis's Clausifier *} |
7 section {* Example that Exercises Metis's Clausifier *} |
8 |
8 |
9 theory Clausification |
9 theory Clausification |
10 imports Complex_Main |
10 imports Complex_Main |
11 begin |
11 begin |
12 |
12 |