| changeset 42463 | f270e3e18be5 | 
| parent 42208 | 02513eb26eb7 | 
| child 45035 | 60d2c03d5c70 | 
--- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy Fri Apr 22 15:57:43 2011 +0200 +++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy Sat Apr 23 13:00:19 2011 +0200 @@ -19,7 +19,7 @@ typedecl key typedecl room -types keycard = "key \<times> key" +type_synonym keycard = "key \<times> key" record state = owns :: "room \<Rightarrow> guest option"