src/HOL/Tools/record.ML
changeset 51552 c713c9505f68
parent 51551 88d1d19fb74f
child 51685 385ef6706252