src/HOL/Record.thy
changeset 81577 a712bf5ccab0
parent 81137 52ed95fa4656
child 81742 4b739ed65946