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