src/HOL/Tools/record.ML
changeset 33649 854173fcd21c
parent 33612 2640cc1cfc2e
child 33691 3db22a5707f3