equal
deleted
inserted
replaced
4 |
4 |
5 datatype guest = Guest0 | Guest1 |
5 datatype guest = Guest0 | Guest1 |
6 datatype key = Key0 | Key1 | Key2 | Key3 |
6 datatype key = Key0 | Key1 | Key2 | Key3 |
7 datatype room = Room0 |
7 datatype room = Room0 |
8 |
8 |
9 types card = "key * key" |
9 type_synonym card = "key * key" |
10 |
10 |
11 datatype event = |
11 datatype 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" |