src/HOL/Tools/record.ML
changeset 44182 ecb51b457064
parent 44121 44adaa6db327
child 44653 6d8d09b90398