src/HOL/Record.thy
changeset 67341 df79ef3b3a41
parent 67091 1393c2340eec
child 69605 a96320074298