src/HOL/Tools/record.ML
changeset 48442 3c9890c19e90
parent 48272 db75b4005d9a
child 49833 1d80798e8d8a