src/HOL/Tools/recdef_package.ML
changeset 21790 9d2761d09d91
parent 21505 13d4dba99337
child 22101 6d13239d5f52