src/HOL/Record.thy
changeset 54614 689398f0953f
parent 54147 97a8ff4e4ac9
child 55066 4e5ddf3162ac