src/HOL/Tools/record.ML
changeset 47647 ec29cc09599d
parent 47234 0599911c2bf5
child 47783 0eadfb89badb