src/HOL/Tools/record.ML
changeset 43448 90aec5043461
parent 43329 84472e198515
child 43681 66f349cff1fb