src/HOL/Tools/record.ML
changeset 76290 64d29ebb7d3d
parent 76040 5326abe1fff8
child 77885 89676df5846a
equal deleted inserted replaced
76289:a6cc15ec45b2 76290:64d29ebb7d3d