src/HOL/Tools/record.ML
changeset 37979 0f21ebea4a73
parent 37781 2fbbf0a48cef
child 38012 3ca193a6ae5a