src/HOL/Tools/record.ML
changeset 41171 043f8dc3b51f
parent 40845 15b97bd4b5c0
child 41489 8e2b8649507d