src/HOL/Record.thy
changeset 11837 b2a9853ec6dd
parent 11833 475f772ab643
child 11956 b814360b0267