src/HOL/Tools/record.ML
changeset 60292 ba3c716144dd
parent 59936 b8ffc3dc9e24
child 60326 68699e576d51