src/HOL/Record.thy
changeset 5924 b9d5f5901b59
parent 5732 8712391bbf3d
child 7357 d0e16da40ea2