src/HOL/Tools/recdef_package.ML
changeset 11115 285b31e9e026
parent 10775 3a5e5657e41c
child 11629 481148b273b5