src/HOL/Tools/record.ML
changeset 40065 1e4c7185f3f9
parent 39557 fe5722fce758
child 40315 11846d9800de