src/HOL/record.ML
changeset 4504 2f39aa4bebf3
parent 4459 4066db36616b
child 4564 dc45cf21dbd2