src/HOL/Tools/record.ML
changeset 41836 c9d788ff7940
parent 41591 484eedf607da
child 41926 b09a67a3dc1e