src/HOL/Tools/record_package.ML
changeset 24027 a1afcff544a6
parent 23578 5ca3b23c09ed
child 24219 e558fe311376