HOL-ex.Datatype_Record_Examples