equal
deleted
inserted
replaced
3 Author: Stefan Berghofer and Markus Wenzel, TU Muenchen |
3 Author: Stefan Berghofer and Markus Wenzel, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header {* Datatypes *} |
6 header {* Datatypes *} |
7 |
7 |
8 theory Datatype = Datatype_Universe: |
8 theory Datatype |
|
9 import Datatype_Universe |
|
10 begin |
9 |
11 |
10 subsection {* Representing primitive types *} |
12 subsection {* Representing primitive types *} |
11 |
13 |
12 rep_datatype bool |
14 rep_datatype bool |
13 distinct True_not_False False_not_True |
15 distinct True_not_False False_not_True |