src/HOL/Tools/record.ML
changeset 37225 32c5251f78cd
parent 37186 349e9223c685
child 37469 1436d6f28f17