src/HOL/Tools/record_package.ML
changeset 25154 6155f2faf23e
parent 25070 e2a39b6526b0
child 25179 b84f3c3c27f2