src/HOL/Tools/record.ML
changeset 48712 6b7a9bcc0bae
parent 48272 db75b4005d9a
child 49833 1d80798e8d8a