src/HOL/Tools/record.ML
changeset 36034 ee84eac07290
parent 35994 9cc3df9a606e
child 36137 0be811a98d3a