src/HOL/Tools/record.ML
changeset 39650 2a35950ec495
parent 39557 fe5722fce758
child 40315 11846d9800de