src/HOL/Tools/recdef_package.ML
changeset 10783 2781ac7a4619
parent 10775 3a5e5657e41c
child 11629 481148b273b5