src/HOL/Tools/record.ML
changeset 73616 b0ea03e837b1
parent 71214 5727bcc3c47c
child 74282 c2ee8d993d6a
equal deleted inserted replaced
73615:e768759ce6c5 73616:b0ea03e837b1