src/HOL/Record.thy
changeset 55965 0c2c61a87a7d
parent 55066 4e5ddf3162ac
child 56047 1f283d0a4966