src/HOL/Tools/record.ML
changeset 56024 0921c1dc344c
parent 54895 515630483010
child 56245 84fc7dfa3cd4