src/HOL/Tools/record.ML
changeset 43333 2bdec7f430d3
parent 43329 84472e198515
child 43681 66f349cff1fb