src/HOL/Tools/record.ML
changeset 41648 6d736d983d5c
parent 41591 484eedf607da
child 41926 b09a67a3dc1e