src/HOL/Record.thy
changeset 45300 d8c8c2fcab2c
parent 44922 14f7da460ce8
child 46950 d0181abdbdac