src/HOL/Tools/record_package.ML
changeset 13660 e36798726ca4
parent 13462 56610e2ba220
child 13904 c13e6e218a69