src/HOL/Tools/record.ML
changeset 45476 6f9e24376ffd
parent 45434 f28329338d30
child 45620 f2a587696afb