src/HOL/Tools/record.ML
changeset 58084 9f77084444df
parent 57983 6edc3529bb4e
child 58187 d2ddd401d74d