src/HOL/Tools/record.ML
changeset 42224 578a51fae383
parent 42086 74bf78db0d87
child 42242 39261908e12f