src/HOL/Record.thy
changeset 7025 afbd8241797b
parent 5732 8712391bbf3d
child 7357 d0e16da40ea2