src/HOL/Tools/record.ML
changeset 38386 370712dd4628
parent 38252 175a5b4b2c94
child 38401 c4de81b7fdec