src/HOL/Record.thy
changeset 82218 cbf9f856d3e0
parent 81742 4b739ed65946