src/HOL/Tools/record.ML
changeset 49445 638cefe3ee99
parent 48272 db75b4005d9a
child 49833 1d80798e8d8a