src/HOL/Record.thy
changeset 55487 6380313b8ed5
parent 55066 4e5ddf3162ac
child 56047 1f283d0a4966