src/HOL/Record.thy
changeset 5253 82a5ca6290aa
parent 5210 54aaa779b6b4
child 5694 39af7b3dd1c4