src/HOL/Record.thy
changeset 5526 e7617b57a3e6
parent 5210 54aaa779b6b4
child 5694 39af7b3dd1c4