src/HOL/Tools/record.ML
changeset 42190 b6b5846504cd
parent 42086 74bf78db0d87
child 42242 39261908e12f