src/HOL/Record.thy
changeset 5807 bd2d9dd34dfd
parent 5732 8712391bbf3d
child 7357 d0e16da40ea2