src/HOL/Tools/recdef_package.ML
changeset 29380 a9ee3475abf4
parent 29006 abe0f11cfa4e
child 29579 cb520b766e00