src/HOL/Tools/record.ML
changeset 37819 000049335247
parent 37781 2fbbf0a48cef
child 38012 3ca193a6ae5a