src/HOL/Tools/record.ML
changeset 41752 949eaf045e00
parent 41591 484eedf607da
child 41926 b09a67a3dc1e