src/HOL/record.ML
changeset 4527 4878fb3d0ac5
parent 4459 4066db36616b
child 4564 dc45cf21dbd2