src/HOL/Tools/record.ML
changeset 74517 dc1a7c10565b
parent 74383 107941e8fa01
child 74537 44e4f09b1cc4