src/HOL/Record.thy
changeset 6590 fa5f2ca893c5
parent 5732 8712391bbf3d
child 7357 d0e16da40ea2