src/HOL/Tools/recdef_package.ML
changeset 11193 851c90b23a9e
parent 10775 3a5e5657e41c
child 11629 481148b273b5