src/HOL/Tools/record.ML
changeset 36928 637100169bc7
parent 36610 bafd82950e24
child 36945 9bec62c10714