equal
deleted
inserted
replaced
1 theory Hotel_Example |
1 theory Hotel_Example |
2 imports Main |
2 imports Main |
3 begin |
3 begin |
4 |
4 |
5 datatype guest = Guest0 | Guest1 |
5 datatype_new guest = Guest0 | Guest1 |
6 datatype key = Key0 | Key1 | Key2 | Key3 |
6 datatype_new key = Key0 | Key1 | Key2 | Key3 |
7 datatype room = Room0 |
7 datatype_new room = Room0 |
8 |
8 |
9 type_synonym card = "key * key" |
9 type_synonym card = "key * key" |
10 |
10 |
11 datatype event = |
11 datatype_new event = |
12 Check_in guest room card | Enter guest room card | Exit guest room |
12 Check_in guest room card | Enter guest room card | Exit guest room |
13 |
13 |
14 definition initk :: "room \<Rightarrow> key" |
14 definition initk :: "room \<Rightarrow> key" |
15 where "initk = (%r. Key0)" |
15 where "initk = (%r. Key0)" |
16 |
16 |