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