| changeset 42463 | f270e3e18be5 |
| parent 42208 | 02513eb26eb7 |
| child 45035 | 60d2c03d5c70 |
| 42462:0fd80c27fdf5 | 42463:f270e3e18be5 |
|---|---|
17 |
17 |
18 typedecl guest |
18 typedecl guest |
19 typedecl key |
19 typedecl key |
20 typedecl room |
20 typedecl room |
21 |
21 |
22 types keycard = "key \<times> key" |
22 type_synonym keycard = "key \<times> key" |
23 |
23 |
24 record state = |
24 record state = |
25 owns :: "room \<Rightarrow> guest option" |
25 owns :: "room \<Rightarrow> guest option" |
26 currk :: "room \<Rightarrow> key" |
26 currk :: "room \<Rightarrow> key" |
27 issued :: "key set" |
27 issued :: "key set" |