src/HOL/Tools/record.ML
changeset 55807 fd31d0e70eb8
parent 54895 515630483010
child 56245 84fc7dfa3cd4