src/HOL/Tools/record.ML
changeset 55657 d5ad50aea356
parent 54895 515630483010
child 56245 84fc7dfa3cd4