src/HOL/Tools/record.ML
changeset 52451 e64c1344f21b
parent 52230 1105b3b5aa77
child 52788 da1fdbfebd39
equal deleted inserted replaced
52450:e09e1091394d 52451:e64c1344f21b