src/HOL/Tools/record_package.ML
changeset 14472 cba7c0a3ffb3
parent 14427 cea7d2f76112
child 14579 e79f1923fa0a
equal deleted inserted replaced
14471:5688b05b2575 14472:cba7c0a3ffb3