equal
deleted
inserted
replaced
2 Author: Jasmin Blanchette, TU Muenchen |
2 Author: Jasmin Blanchette, TU Muenchen |
3 |
3 |
4 Example that exercises Metis's (and hence Sledgehammer's) type encodings. |
4 Example that exercises Metis's (and hence Sledgehammer's) type encodings. |
5 *) |
5 *) |
6 |
6 |
7 header {* |
7 section {* |
8 Example that Exercises Metis's (and Hence Sledgehammer's) Type Encodings |
8 Example that Exercises Metis's (and Hence Sledgehammer's) Type Encodings |
9 *} |
9 *} |
10 |
10 |
11 theory Type_Encodings |
11 theory Type_Encodings |
12 imports Main |
12 imports Main |