src/HOL/Tools/record.ML
changeset 60292 ba3c716144dd
parent 59936 b8ffc3dc9e24
child 60326 68699e576d51
equal deleted inserted replaced
60291:4335ee20014e 60292:ba3c716144dd