src/HOL/Tools/record_package.ML
changeset 5253 82a5ca6290aa
parent 5235 c404f25c58e8
child 5290 b755c7240348