src/HOL/Tools/record.ML
changeset 44262 355d5438f5fb
parent 44121 44adaa6db327
child 44653 6d8d09b90398