| changeset 58130 | 5e9170812356 |
| parent 56798 | 939e88e79724 |
| child 58310 | 91ea607a34d8 |
| 58129:3ec65a7f2b50 | 58130:5e9170812356 |
|---|---|
1 theory Complex_Types |
1 theory Complex_Types |
2 imports SPARK |
2 imports "../SPARK" |
3 begin |
3 begin |
4 |
4 |
5 datatype day = Mon | Tue | Wed | Thu | Fri | Sat | Sun |
5 datatype_new day = Mon | Tue | Wed | Thu | Fri | Sat | Sun |
6 |
6 |
7 record two_fields = |
7 record two_fields = |
8 Field1 :: "int \<times> day \<Rightarrow> int" |
8 Field1 :: "int \<times> day \<Rightarrow> int" |
9 Field2 :: int |
9 Field2 :: int |
10 |
10 |