src/HOL/Record.thy
changeset 34272 95df5e6dd41c
parent 34151 8d57ce46b3f7
child 35132 d137efecf793