src/HOL/Tools/record.ML
changeset 46138 85f8d8a8c711
parent 46056 4dba48d010d5
child 46186 9ae331a1d8c5