src/HOL/Tools/record.ML
changeset 51430 e96447ea13c9
parent 51143 0a2371e7ced3
child 51551 88d1d19fb74f