5.1.3 Notes on specifying user-defined records